proposition: Lemma ord_le_trans: forall alpha beta gamma:Ordinal, alpha <= beta -> beta <= gamma -> alpha <= gamma.
proof: Proof. induction alpha. induction beta. induction gamma. intros. apply ord_le_respects_succ. apply IHalpha with beta. apply ord_le_respects_succ_converse; trivial. apply ord_le_respects_succ_converse; trivial. intros. apply ord_le_S_sup_converse in H1. destruct H1 as [i]. apply ord_le_S_sup with i. apply H; trivial. intros. pose proof (ord_sup_minimal_converse _ _ _ H1). apply ord_le_S_sup_converse in H0. destruct H0 as [i]. apply H with i; trivial. intros. pose proof (ord_sup_minimal_converse _ _ _ H0). constructor. intro. apply H with beta; trivial. Qed.
imports: Classical