proposition: Lemma omega_limit : strict_lub T1nat T1omega.
proof: Proof. split. - intro i; destruct i; compute; auto. - intros alpha H . assert (Hnf : nf alpha) by eapply (LE_nf_r (H 0)). + destruct (LT_eq_LT_dec nf_omega Hnf ) as [[H0 | H0] | H0]. * now apply LE_r. * subst; now apply LE_refl. * destruct (lt_omega_inv H0). { subst . specialize (H 1). destruct (LE_LT_eq_dec H). destruct (not_LT_zero l). discriminate. } { destruct H1 as [n H3]. subst ; generalize (H (S (S n))). intro H2. destruct (le_inv (LE_le H2)) as [H1 | H1]. - destruct (not_lt_zero H1). - destruct H1 as [[_ H3] | [_ [H3 _]]]. + destruct (Nat.nlt_succ_diag_l _ H3). + destruct (Nat.neq_succ_diag_l _ H3). } 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)