proposition: Lemma ord_total_order: forall alpha beta:Ordinal, alpha < beta \/ alpha == beta \/ alpha > beta.
proof: Proof. induction alpha. - induction beta. + destruct (IHalpha beta) as [|[|]]. * left; apply ord_lt_respects_succ; trivial. * right; left. split. -- apply ord_le_respects_succ; apply H. -- apply ord_le_respects_succ; apply H. * right; right. apply ord_lt_respects_succ; trivial. + destruct (classic (exists i:I, ordS alpha < o i)). * destruct H0 as [i]. left. apply ord_lt_le_trans with (o i); trivial. apply ord_le_sup. * destruct (classic (exists i:I, ordS alpha == o i)). -- destruct H1 as [i]. right; left. split. ++ apply ord_le_trans with (o i). ** apply H1. ** apply ord_le_sup. ++ apply ord_sup_minimal. intro. destruct (H i0) as [|[|]]. ** contradiction H0; exists i0; trivial. ** apply H2. ** apply ord_lt_le; trivial. -- assert (forall i:I, ordS alpha > o i). ++ intros. destruct (H i) as [|[|]]. ** contradiction H0; exists i; trivial. ** contradiction H1; exists i; trivial. ** trivial. ++ right; right. apply ord_le_lt_trans with alpha. ** apply ord_sup_minimal. intro. apply ord_le_respects_succ_converse. apply H2. ** apply ord_le_refl. - induction beta. + case (classic (exists i:I, o i > ordS beta)); intro. * destruct H0 as [i]. right; right. apply ord_lt_le_trans with (o i); trivial. apply ord_le_sup. * case (classic (exists i:I, o i == ordS beta)); intro. -- right; left. destruct H1 as [i]. split. ++ apply ord_sup_minimal. intro j. destruct (H j (ordS beta)) as [|[|]]. ** apply ord_lt_le; trivial. ** apply H2. ** contradiction H0; exists j; trivial. ++ apply ord_le_trans with (o i). ** apply H1. ** apply ord_le_sup. -- left. apply ord_le_respects_succ. apply ord_sup_minimal. intro. destruct (H i (ordS beta)) as [|[|]]. ++ apply ord_le_respects_succ_converse; trivial. ++ contradiction H1; exists i; trivial. ++ contradiction H0; exists i; trivial. + case (classic (exists j:I0, ord_sup o < o0 j)); intro. * left. destruct H1 as [j]. apply ord_lt_le_trans with (o0 j); trivial. apply ord_le_sup. * case (classic (exists i:I, o i > ord_sup o0)); intro. -- destruct H2 as [i]. right; right. apply ord_lt_le_trans with (o i); trivial. apply ord_le_sup. -- right; left. split. ++ apply ord_sup_minimal; intro. destruct (H i (ord_sup o0)) as [|[|]]. ** apply ord_lt_le; trivial. ** apply H3. ** contradiction H2; exists i; trivial. ++ apply ord_sup_minimal; intro j. destruct (H0 j) as [|[|]]. ** contradiction H1; exists j; trivial. ** apply H3. ** apply ord_lt_le; trivial. Qed.
imports: Coq(Classical) Coq(Eqdep)