proposition: Theorem lt_trans: forall alpha beta gamma: T1, lt alpha beta -> lt beta gamma -> lt alpha gamma.
proof: Proof. induction alpha, beta, gamma. 1-7: easy. intros Hab Hbc. apply lt_inv_strong in Hab as [Hlt_ab | Heq_ab Hltn_ab | Heq_ab Heqn_ab Hlt_ab]; apply lt_inv_strong in Hbc as [Hlt_bc | Heq_bc Hltn_bc | Heq_bc Heqn_bc Hlt_bc]; subst. 2-4,7: now apply head_lt. 2-4: apply coeff_lt; lia. + now apply head_lt, (IHalpha1 beta1 gamma1). + now apply tail_lt, (IHalpha2 beta2 gamma2). 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)