proposition: Lemma omega_is_limit : Limit omega.
proof: Proof. split. + exists (fin 8); constructor. auto with arith. + inversion 1; subst. * assert (a= 0) by lia; subst a. exists (0, S b); split. -- constructor 2; auto. -- constructor 1; auto. * exfalso; lia. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)