proposition: Lemma oplus_strict_mono_r : forall a b c, nf a -> nf b -> nf c -> lt b c -> lt (a o+ b) (a o+ c).
proof: Proof. Proof with auto with T1. intros. apply oplus_strict_mono_0 with (phi0 (max a c)); trivial. apply nf_phi0;apply max_nf; trivial. apply le_lt_trans with (max a c). - apply le_max_a. - apply lt_a_phi0_a ... - apply le_lt_trans with (max a c) ... apply le_max_b ... Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)