proposition: Lemma lt_plus_l: forall {a b c : T1} {n:nat}, lt a (a + cons b n c).
proof: Proof. induction a; intros *. - apply zero_lt. - simpl. compare destruct a1 b as Hcomp. + apply coeff_lt; lia. + now apply head_lt. + apply tail_lt, IHa2. 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)