proposition: Lemma oplus_eq_rw : forall a n b n' b', cons a n b o+ cons a n' b'= cons a (S (n+n')%nat) (b o+ b').
proof: Proof. intros a n b n' b'; generalize (compare_refl a); intro H; cbn ; now rewrite H. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)