proposition: Lemma oplus_strict_mono_LT_l (alpha beta gamma : T1) : nf gamma -> alpha t1< beta -> alpha o+ gamma t1< beta o+ gamma.
proof: Proof. intros Hgamma H. generalize (LT_nf_l H), (LT_nf_r H); intros Ha Hb. repeat split. now apply oplus_nf. apply oplus_strict_mono_l; trivial. auto with T1. now apply oplus_nf. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)