proposition: Lemma ordinal_obi_lt : forall o x y, is_ordinal o -> lt (obi o) x y = (inc x y & inc y o).
proof: Proof. ir. ap iff_eq; ir. ee. uh H0; ee. rwi obi_leq H0. ee. ap ordinal_strict_sub_inc. apply ordinal_inc_ordinal with o; am. apply ordinal_inc_ordinal with o; am. uhg; ee; am. uh H0; ee. uh H0; ee. rwi obi_U H2; am. ee. uhg; ee. rw obi_leq. ee; try am. cp ordinal_inc_sub. ufi sub H2. apply H2 with y. am. am. am. ap ordinal_inc_sub. apply ordinal_inc_ordinal with o; am. am. uhg; ir. apply ordinal_not_inc_itself with x. apply ordinal_inc_ordinal with o. am. rw H2; am. wri H2 H0; am. Qed.
imports: Arith transfinite