proposition: Lemma ord_le_sup': forall beta:Ordinal, beta <= beta /\ forall (I:Type) (alpha:I->Ordinal) (i:I), beta <= alpha i -> beta <= ord_sup alpha.
proof: Proof. induction beta. - destruct IHbeta. split. + apply ord_le_respects_succ; trivial. + intros. apply ord_le_S_sup with i. assumption. - split. + apply ord_sup_minimal. intro. destruct (H i). apply H1 with i; trivial. + intros J alpha j ?. apply ord_sup_minimal. intro. destruct (H i). apply H2 with j. apply ord_le_trans with (ord_sup o). * apply H2 with i; trivial. * assumption. Qed.
imports: Coq(Classical) Coq(Eqdep)