proposition: Lemma limit_exists: { lim : option A | exists i, forall j, i <= j -> f j = lim }.
proof: Proof. apply constructive_definite_description. destruct (classic (forall i, f i = None)) as [DIV|TERM]. - exists None; split. + exists O; auto. + intros lim (i & LIM). rewrite <- (DIV i). apply LIM; lia. - apply not_all_ex_not in TERM. destruct TERM as (i & TERM). exists (f i); split. + exists i; intros. destruct (f_mono i j H). congruence. auto. + intros lim (i2 & LIM2). set (j := Nat.max i i2). rewrite <- (LIM2 j) by lia. destruct (f_mono i j). lia. congruence. auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)