proposition: Lemma l_R0 : forall n, f n = false.
proof: Proof. assert (H : forall n, Bn n = 0). intros n. apply Rle_antisym. rewrite <- Hl; apply l_maj. apply Bn_pos. intros n; induction n. assert (H1 : Bn 1 = 0); [exact (H 1%nat)|]. unfold Bn, fp in H1. destruct (f 0). simpl in H1; rewrite Rplus_0_l in H1. rewrite Rmult_1_r in H1; symmetry in H1. eelim Rlt_not_eq; [apply Rlt_0_inv_2|assumption]. reflexivity. assert (Hn : Bn (S (S n)) = 0); [exact (H (S (S n)))|]. replace (Bn (S (S n))) with (Bn (S n) + fp (f (S n)) (S n)) in Hn by reflexivity. unfold fp in Hn. destruct (f n). discriminate IHn. destruct (f (S n)). replace (Bn (S n)) with 0 in Hn by (symmetry; apply H). rewrite Rplus_0_l in Hn. assert (Hc : forall m, (/ 2) ^ m > 0). intros m; induction m; simpl. apply Rlt_0_1. apply Rmult_lt_0_compat. apply Rlt_0_inv_2. assumption. eelim Rgt_not_eq; [apply Hc|apply Hn]. reflexivity. Qed.
imports: Reals Lia Lra