proposition: Lemma oplus_lt1 : forall a b, nf a -> nf b -> T1.lt T1.zero a -> T1.lt b (b o+ a).
proof: Proof. destruct a. - intros b _ _ H; T1_inversion H. - intros; now apply oplus_lt_0. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)