proposition: Lemma ordinal_leq_inc_tack_on : forall o x:E, is_ordinal o -> ordinal_leq x o = inc x (tack_on o o).
proof: Proof. ir. ap iff_eq; ir. nin (ordinal_if_leq_or H0). rw tack_on_inc; ap or_introl. rwi ordinal_lt_rw H1. ee; am. rw tack_on_inc; ap or_intror. am. rwi tack_on_inc H0. nin H0. rwi ordinal_inc_rw H0. ee. uh H1; ee. uhg; ee; am. am. rw H0; uhg; ee. am. am. uhg; ir; am. Qed.
imports: Arith transfinite