proposition: Lemma LT_cons_0 : forall a n b a' b', cons a n b t1< cons a' 0 b' -> a t1< a' \/ n = 0 /\ a = a' /\ b t1< b'.
proof: Proof. intros a n b x c H; case (LT_inv H). - now left. - intros (e, H0); subst x; case H0; intro H1. + abstract lia. + case H1; right; auto. 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)