proposition: Lemma oplus_of_phi0 : forall a b, phi0 a o+ phi0 b = match compare a b with Lt => cons b 0 (cons a 0 T1.zero) | Eq => cons a 1 T1.zero | Gt => cons a 0 (cons b 0 T1.zero) end.
proof: Proof. intros a b; now rewrite oplus_of_phi0_0, compare_of_phi0. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)