proposition: Lemma ord_successor_or_limit: forall alpha:Ordinal, successor_ordinal alpha \/ limit_ordinal alpha.
proof: Proof. induction alpha. left; constructor. destruct (classic (forall i:I, exists j:I, o i < o j)). right; constructor; trivial. destruct (not_all_ex_not _ _ H0) as [i]. assert (forall j:I, o j <= o i). intro. destruct (ord_total_order (o i) (o j)) as [|[|]]. contradiction H1; exists j; trivial. apply H2. apply ord_lt_le; trivial. assert (ord_sup o == o i). split. apply ord_sup_minimal; trivial. apply ord_le_sup. case (H i); intro. left; apply succ_ord_wd with (o i); trivial. split; apply H3. right. apply limit_ord_wd with (o i); trivial. split; apply H3. Qed.
imports: Classical