proposition: Lemma ordinal_tack_on : forall o:E, is_ordinal o -> is_ordinal (tack_on o o).
proof: Proof. ir. uhg. apply by_cases with (inc o o); ir. assert (tack_on o o = o). ap extensionality; uhg; ir. rwi tack_on_inc H1; nin H1. am. rw H1; am. rw tack_on_inc. ap or_introl; am. rw H1; am. change (is_leq_gen_scale ID (tack_on o (ID o))). ap leq_gen_scale_tack_on. exact H. am. Qed.
imports: Arith transfinite