proposition: Lemma oplus_strict_mono_l : forall a b c, nf a -> nf b -> nf c -> T1.lt a b -> T1.lt (a o+ c) (b o+ c).
proof: Proof. intros a b c Ha Hb Hc H. rewrite (oplus_comm Ha Hc). rewrite (oplus_comm Hb Hc). now apply oplus_strict_mono_r. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)