proposition: Lemma oplus_lt2 : forall a b, nf a -> nf b -> T1.lt T1.zero b -> T1.lt a (b o+ a).
proof: Proof. intros a b Ha Hb HD. rewrite (oplus_comm Hb Ha); auto; apply oplus_lt1;auto. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)