proposition: Lemma ord_le_sup: forall (I:Type) (alpha:I->Ordinal) (i:I), alpha i <= ord_sup alpha.
proof: Proof. assert (forall beta:Ordinal, beta <= beta /\ forall (I:Type) (alpha:I->Ordinal) (i:I), beta <= alpha i -> beta <= ord_sup alpha). induction beta. destruct IHbeta. split. apply ord_le_respects_succ; trivial. intros. apply ord_le_S_sup with i. trivial. 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. trivial. intros. destruct (H (alpha i)). apply H1 with i; trivial. Qed.
imports: Classical