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