proposition: Lemma ordinal_obi_next_compatible : forall o:E, is_ordinal o -> next_compatible ID (obi o).
proof: Proof. ir. cp H; uh H. uh H. nin H. ee. assert (same_order x (obi o)). uhg; ee; ap show_is_suborder. do 5 (uh H1; ee; try am). ap obi_axioms. ir. wr H. rw ordinal_leq_obi. am. am. uh H2; ee; am. uh H2; ee; am. ap obi_axioms. do 5 (uh H1; ee; try am). ir. wr ordinal_leq_obi. rw H; am. am. uh H2; ee. rwi obi_U H2; rw H; am. uh H2; ee. rwi obi_U H3; rw H; am. uhg; dj. apply wo_same_order with x. am. uh H1; ee; am. rw ordinal_punctured_downward. tv. am. rwi obi_U H4; am. Qed.
imports: Arith transfinite