proposition: Lemma finite_tack_on : forall x y, is_finite x -> is_finite (tack_on x y).
proof: Proof. ir. uhg; ir. pose (g:= fun z => Transposition.create y (f y) (f z)). util (finite_tack_on_case (x:=x) (y:=y) (f:=g)). am. uhg; ee. uhg; ir. uh H0; ee. cp (H0 x0 H1). apply by_cases with (f x0 = f y); ir. uf g. rw H4. rw Transposition.i_j_j. rw tack_on_inc; ap or_intror; tv. apply by_cases with (f x0 = y); ir. uf g. rw H5. rw Transposition.i_j_i. util (H0 y). rw tack_on_inc; ap or_intror; tv. am. uf g. rw Transposition.not_i_not_j; try am. uhg; ir. uh H0; ee. ap H4; try am. apply Transposition.inj with y (f y). am. uf g. rw Transposition.i_j_j. tv. uhg; ee; try lu. uhg; ee; try lu. uhg; ir. assert (inc (Transposition.create y (f y) x0) (tack_on x y)). apply by_cases with (x0 = y); ir. rw H3; rw Transposition.i_j_i. uh H0; ee; ap H0. rw tack_on_inc; ap or_intror; tv. apply by_cases with (x0 = f y); ir. rw H4; rw Transposition.i_j_j. rw tack_on_inc; ap or_intror; tv. rw Transposition.not_i_not_j; try am. uh H1; ee. uh H4; ee. cp (H6 _ H3). nin H7. sh x1; ee; try am. apply Transposition.inj with y (f y). am. Qed.
imports: Arith ordinal