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