proposition: Lemma plus_smono_LT_r (alpha:T1) : forall beta gamma, nf alpha -> beta t1< gamma -> alpha + beta t1< alpha + gamma.
proof: Proof. destruct 2 as [H1 [H2 H3]]; split. apply plus_nf; auto. split. now apply reduce_lt_plus. apply plus_nf; 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)