proposition: Lemma ordinal_if_leq_or : forall a o:E, ordinal_leq a o -> (ordinal_lt a o \/ a = o).
proof: Proof. ir. apply by_cases with (a = o); ir. ap or_intror; am. ap or_introl. uhg; uh H; xd. uhg; ee; am. Qed.
imports: Arith transfinite