proposition: Lemma l_not_R0_partial : exists N, ~(forall n, (n <= N)%nat -> f n = false).
proof: Proof. assert (Hlt : l > 0); [apply Hl_lt_0|]. assert (HN : exists N, forall n, (n >= N)%nat -> (/ 2) ^ n < l). destruct (pow_lt_1_zero (/2)) with l as [N HN]. rewrite Rabs_right; lra. lra. exists N; intros n Hn. pattern ((/ 2) ^ n); rewrite <- Rabs_right. apply HN; assumption. apply Rle_ge; apply pow_le; lra. destruct HN as [N HN]. exists N; intros Hneg. assert (Hc : l <= (/2) ^ N). apply l_partial; assumption. assert (Hk : l > (/2) ^ N). apply HN; constructor. lra. Qed.
imports: Reals Lia Lra