proposition: Lemma ordinal_lt_lt_eq_or : forall a o:E, is_ordinal a -> is_ordinal o -> (ordinal_lt a o \/ ordinal_lt o a \/ a=o).
proof: Proof. ir. nin (ordinal_leq_leq_or H H0). nin (ordinal_if_leq_or H1). ap or_introl. am. ap or_intror. ap or_intror. am. nin (ordinal_if_leq_or H1). ap or_intror. ap or_introl; am. ap or_intror; ap or_intror; sy; am. Qed.
imports: Arith transfinite