proposition: Lemma remove_first_sumand : forall a n b b', cons a n b t1< cons a n b' -> b t1< b'.
proof: Proof. intros a n b b' H; apply LT_inv in H. destruct H. - destruct H as [_ [H _] ]. now apply lt_irrefl in H. - destruct H as [_ [H | [ _ H]]]; auto. destruct (Nat.lt_irrefl _ H). 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)