proposition: Lemma oplus_eqn : forall a b, a o+ b = match a, b with T1.zero, _ => b | _, T1.zero => a | cons a1 n1 b1, cons a2 n2 b2 => match compare a1 a2 with Gt => cons a1 n1 (b1 o+ b) | Eq => cons a1 (S (n1 + n2)) (b1 o+ b2) | Lt => cons a2 n2 (a o+ b2) end end.
proof: Proof. destruct a, b; now cbn. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)