proposition: Lemma omega_is_limit : Limit omega.
proof: Proof. split. + exists (inl 0); constructor. + inversion 1; subst. exists (inl (S x)); split; constructor;auto with arith. abstract lia. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)