proposition: Lemma ordinal_leq_gen_tack_on : forall o:E, is_ordinal o -> leq_gen ID o (tack_on o o).
proof: Proof. ir. pose (u:=tack_on o o). assert (is_ordinal u). uf u; ap ordinal_tack_on; am. assert (ordinal_lt o u). rw ordinal_lt_rw. ee; try am. uf u; rw tack_on_inc; ap or_intror; tv. pose (q:= tack_on u u). assert (is_ordinal q). uf q; ap ordinal_tack_on; am. assert (ordinal_lt u q). rw ordinal_lt_rw. ee; try am. uf q; rw tack_on_inc; ap or_intror; tv. cp H2; uh H4; uh H4; nin H4; ee. assert (u = next x u). sy; transitivity (ID u). apply (next_compatible_scale (f:= ID)). am. cp H0. uh H6; uh H6; nin H6; ee. wr H6. apply next_comp_sub_scale with (f:= ID). am. am. rw H6; rw H4. uh H3; ee. uh H3; ee; am. rw H4. rwi ordinal_lt_rw H3; ee. rwi ordinal_inc_rw H6; ee; am. tv. rw (leq_gen_leq (f:=ID)(a:=x)). assert (lt x o u). rw H6; ap next_compatible_lt. uh H0; uh H0; nin H0; ee. wr H0; apply next_comp_sub_scale with (f:= ID). am. am. rw H0; rw H4. uh H3; ee. uh H3; ee; am. rwi ordinal_lt_rw H3. ee. rwi ordinal_inc_rw H7. ee. rw H4; am. am. rwi ordinal_lt_rw H1; ee; am. uh H7; ee; am. am. rw H4. uf q; rw tack_on_inc; ap or_introl. uf u; rw tack_on_inc; ap or_intror; tv. rw H4; uf q; rw tack_on_inc; ap or_intror; tv. Qed.
imports: Arith transfinite