proposition: Lemma oplus_strict_mono_bi : forall a b c d , nf a -> nf b -> nf c -> nf d -> T1.lt a b -> T1.lt c d -> T1.lt (a o+ c) (b o+ d).
proof: Proof. intros a b c d Ha Hb Hc Hd H0 H1; apply lt_trans with (oplus a d). - apply oplus_strict_mono_r; auto. - apply oplus_strict_mono_l; auto. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)