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