proposition: Lemma finite_invariant : forall y, (exists x, are_isomorphic x y & is_finite x) -> is_finite y.
proof: Proof. ir. nin H. ee. rwi iso_trans_ex_rw H. nin H. uhg. ir. pose (g:= fun z => (inverse x x0 (f (x0 z)))). cp (Transformation.bijective_inverse H). assert (are_inverse y x (inverse x x0) x0). uhg; ee; lu. cp (Transformation.inverse_bijective H3). uh H0. util (H0 g). uhg. ee. uf g. uhg; ir. uh H4; ee. uh H4. ap H4. uh H1; ee; uh H1. ap H1. uh H; ee; uh H; ap H. am. uf g; uhg; ir. uh H; ee. uh H9; ee. ap H10. am. am. uh H1; ee. ap H11. ap H. am. ap H. am. uh H4; ee. uh H13; ee. ap H14. ap H1. ap H; am. ap H1; ap H; am. am. uhg; ee; try lu. uhg. ee; try lu. uhg. ir. uh H5; ee. uh H7; ee. util (H9 (inverse x x0 x1)). uh H4; ee. ap H4. am. nin H10; ee. sh (x0 x2). ee. uh H; ee; ap H. am. uh H4; ee. uh H13; ee. ap H14. uh H1; ee; ap H1. uh H; ee; ap H. am. am. am. Qed.
imports: Arith ordinal