proposition: Lemma decompose (i j : nat): (i,j) = omega * i + j.
proof: Proof. destruct i, j; cbn; (reflexivity || (try f_equal; lia)). Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)