proposition: Lemma omega_not_succ : forall alpha, ~ Successor omega alpha.
proof: Proof. destruct alpha as [n | n]. - apply Successor_inv3. - intro H; apply Successor_inv2 in H; discriminate. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)