proposition: Lemma oplus_lt_rw : forall a n b a' n' b', T1.lt a a' -> cons a n b o+ cons a' n' b'= cons a' n' (cons a n b o+ b').
proof: Proof. intros a n b a' n' b' H; cbn. now apply compare_lt_iff in H as ->. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)