proposition: Lemma strict_lub_T1limit : forall (alpha :T1)(s : nat -> T1), nf alpha -> strict_lub s alpha -> T1limit alpha.
proof: Proof. destruct 2. destruct (zero_limit_succ_dec H). destruct s0. - subst. destruct (not_LT_zero (H0 0)). - assumption. - destruct s0 as [beta [H2 H3]]. subst. specialize (H1 beta ). assert (forall i, s i t1<= beta). { intro i. apply LT_succ_LE_2;auto. } generalize (H1 H3). intro H4. absurd (beta t1< beta). apply LT_irrefl. apply LT_LE_trans with (succ beta);auto. now apply LT_succ. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)