proposition: Lemma LT_add (alpha beta : T1): nf alpha -> nf beta -> beta <> zero -> alpha t1< alpha + beta.
proof: Proof. intros H H0 H1. rewrite <- plus_zero_r at 1. apply plus_smono_LT_r; auto. apply not_zero_lt; 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)