proposition: Lemma ordinal_lt_tack_on_leq : forall a o:E, is_ordinal a -> (ordinal_lt a o = ordinal_leq (tack_on a a) o).
proof: Proof. ir. ap iff_eq; ir. cp H0. rwi ordinal_lt_rw H1. ee. uhg; ee. ap ordinal_tack_on; am. am. uhg; ir. rwi tack_on_inc H3; nin H3. uh H0; ee. uh H0; ee. ap H6; am. rw H3; am. uhg; ee. uhg; ee; try am. uh H0; ee; am. uh H0; ee. uhg; ir. ap H2. rw tack_on_inc. ap or_introl; am. uhg; ir. uh H0; ee. apply ordinal_not_inc_itself with a. am. rw H1. ap H3. rw tack_on_inc. ap or_intror; sy; am. Qed.
imports: Arith transfinite