proposition: Lemma ord_le_S_sup_converse: forall (alpha:Ordinal) (J:Type) (beta:J->Ordinal), ordS alpha <= ord_sup beta -> exists j:J, ordS alpha <= beta j.
proof: Proof. intros. inversion H. exists j. assumption. Qed.
imports: Classical