proposition: Lemma unique_decomposition (alpha: t) : exists! i j: nat, alpha = omega * i + j.
proof: Proof. destruct alpha as [i j]; exists i; split. - exists j; split. + now rewrite decompose. + intros x; repeat rewrite <- decompose; congruence. - intros x [y [Hy _]]; rewrite <- decompose in Hy; congruence. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)