proposition: Lemma LT_one alpha : alpha t1< one -> alpha = zero.
proof: Proof. intros [H1 [H2 _]]; destruct alpha; auto. destruct (lt_inv H2). - destruct (not_lt_zero H). - decompose [and or] H. 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)