proposition: Lemma l_partial : forall N, (forall n, (n <= N)%nat -> f n = false) -> l <= (/2) ^ N.
proof: Proof. intros N HN. assert (forall n, (n <= N)%nat -> Bn n = 0). intros n H; induction n. reflexivity. replace (Bn (S n)) with (Bn n + fp (f n) n) by reflexivity. rewrite IHn; [|lia]. unfold fp. destruct (Bool.bool_dec (f n) true) as [Hd|Hd]. destruct (Bool.eq_true_false_abs (f n)). assumption. apply HN; lia. destruct (f n) as [|]. elim Hd; reflexivity. ring. assert (Hd : Bn N = 0); [apply H; constructor|]. replace l with (l - Bn N) by (rewrite Hd; ring). apply Bn_l_dist. Qed.
imports: Reals Lia Lra