proposition: Lemma limit_iff (alpha : t) : Limit alpha <-> alpha = omega.
proof: Proof. split. - intro H; now apply limit_is_omega. - intro; subst; apply omega_is_limit. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)