proposition: Lemma lt_fin_iff (i j : nat): lt (T1nat i) (T1nat j) <-> Nat.lt i j.
proof: Proof. destruct i, j. - split; [discriminate | lia]. - split; [ auto with arith| cbn; constructor ]. - split; inversion 1. - split; inversion 1. + unfold compare in H1. simpl in H1. destruct (Nat.compare_spec i j); try discriminate. auto with arith. + apply coeff_lt; auto with arith. + apply coeff_lt; lia. 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)