proposition: Lemma oplus_le1 : forall a b, nf a -> nf b -> leq lt a (a o+ b).
proof: Proof. intros; destruct b. - now rewrite oplus_0_r. - apply lt_incl_le; apply oplus_lt1; auto with T1. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)