proposition: Lemma omega_ap : ap omega.
proof: Proof. split; [discriminate |];intros beta gamma H H0; destruct beta, gamma. inversion H; subst. - inversion H0; subst. + inversion H2; inversion H3; subst; try lia. * unfold plus; destruct n0; left; auto with arith. + abstract lia. - abstract lia. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)