proposition: Lemma f_false : l = 0.
proof: Proof. apply Rle_antisym. apply l_lub. intros n. induction n; simpl. apply Rle_refl. assert (H : f n = false). apply Hf. unfold fp; destruct (f n). discriminate H. rewrite Rplus_0_r; assumption. apply Rle_trans with (Bn 0). apply Rle_refl. apply l_maj. Qed.
imports: Reals Lia Lra