proposition: Lemma limit_is_omega alpha : Limit alpha -> alpha = omega.
proof: Proof. destruct alpha. - intro H; inversion H. destruct n. + destruct H0 as [w Hw]. inversion Hw. abstract lia. + specialize (H1 (inl n)). destruct H1. constructor; auto. destruct H1. inversion H2; subst; inversion H1; subst. abstract lia. - destruct n. + trivial. + destruct 1. specialize (H0 (inr n)). destruct H0. constructor; auto. destruct H0 as [H0 H1]; inversion H1; inversion H0; subst. discriminate. injection H7; intro; subst. abstract lia. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)