proposition: Lemma Omega_as_lub : forall alpha, (forall i, fin i o< alpha) <-> omega o<= alpha.
proof: Proof. intro alpha; destruct (comparable_comp_spec omega alpha). - subst;split. + right. + intros; constructor. - split. + intro H0; destruct alpha as [n | n]. * specialize (H0 n); inversion H0; abstract lia. * destruct n. -- right. -- left;constructor; auto with arith. + inversion 1. * inversion H1; constructor. * subst; constructor. - rewrite (lt_omega alpha) in H; destruct H as [n Hn]; subst; split. + intro H; generalize (H n). intro; assert False by (inversion H0; lia); contradiction. + inversion 1; inversion H0. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)