proposition: Lemma successor_ordinal_not_limit: forall alpha:Ordinal, successor_ordinal alpha -> ~ limit_ordinal alpha.
proof: Proof. intros; red; intro. induction H. inversion_clear H0. induction H as [I beta|]. assert (ord_sup beta <= alpha). apply ord_sup_minimal. intro. apply ord_le_respects_succ_converse. destruct (H i) as [j]. apply ord_le_trans with (beta j); trivial. apply ord_le_trans with (ord_sup beta). apply ord_le_sup. apply H1. contradiction (ord_lt_irrefl alpha). apply ord_le_trans with (ord_sup beta); trivial. apply H1. apply IHlimit_ordinal. split; apply ord_le_trans with beta; (apply H0 || apply H1). contradiction IHsuccessor_ordinal. apply limit_ord_wd with beta; trivial. split; apply H1. Qed.
imports: Classical