proposition: Lemma ord_le_lt_trans: forall alpha beta gamma:Ordinal, alpha <= beta -> beta < gamma -> alpha < gamma.
proof: Proof. intros. apply ord_le_trans with (ordS beta); trivial. apply ord_le_respects_succ; trivial. Qed.
imports: Classical