proposition: Lemma lt_omega alpha : alpha o< omega <-> exists n:nat, alpha = fin n.
proof: Proof. destruct alpha; cbn; split. - inversion_clear 1. + inversion H0. * exists n0; reflexivity. * inversion H1. + inversion H0. - destruct 1. injection H; intros; subst; constructor; auto. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)