proposition: Lemma ordinal_leq_leq_or : forall a o:E, is_ordinal a -> is_ordinal o -> (ordinal_leq a o \/ ordinal_leq o a).
proof: Proof. ir. nin (ordinal_sub_or H H0). ap or_introl. uhg; ee; am. ap or_intror; uhg; ee; am. Qed.
imports: Arith transfinite