proposition: Lemma Omega_limit_limitb alpha s : Omega_limit s alpha -> limitb alpha.
proof: Proof. destruct alpha. destruct 1. destruct n0. - destruct n. + specialize (H 0). inversion H; abstract lia. + now cbn. - destruct (H0 (n, n0)). + right; auto with arith. + specialize (H x). assert ((n,n0) o< s x). apply H1. rewrite lt_succ_le in H2. assert (s x o< s x) by (eapply lt_le_trans; eauto). destruct (ON_mult.lt_strorder Omega Omega) as [H4 H5]. destruct (H4 _ H3). Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)