proposition: Lemma lt_omega alpha : alpha o< omega <-> exists n:nat, alpha = fin n.
proof: Proof. destruct alpha; simpl; split. - inversion_clear 1; exists n; auto. - constructor. - inversion 1; abstract lia. - destruct 1 as [n0 e]; inversion e. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)