proposition: Lemma lt_omega_inv : forall alpha, alpha t1< T1omega -> alpha = zero \/ exists n, alpha = FS n.
proof: Proof. intros alpha [H1 [H2 _]]; destruct alpha; auto. destruct (lt_inv H2). - assert(alpha1 = zero). { apply LT_one. split. subst. eauto with T1. split. auto. now compute. } subst alpha1; right; exists n. generalize (nf_of_finite H1). intro; now subst. - destruct H as [[H3 H4] |[H3 [H4 H5]]]. destruct (Nat.nlt_0_r _ H4). destruct (not_lt_zero H5). 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)