proposition: Lemma l_not_R0 : exists n, f n <> false.
proof: Proof. destruct l_not_R0_partial as [N HN]. induction N. exists 0%nat; intro Hneg. destruct HN. intros n Hn; induction n. assumption. inversion Hn. destruct (Bool.bool_dec (f (S N)) true) as [H|H]. exists (S N); intros Hneg. eapply Bool.eq_true_false_abs; eassumption. apply IHN; intros Hneg. apply Bool.not_true_is_false in H. apply HN; intros n Hn. destruct (eq_nat_dec n (S N)) as [Hd|Hd]. rewrite Hd; assumption. apply Hneg; lia. Qed.
imports: Reals Lia Lra