-intros.
-cut permut (\lambda n.transpose (f (S m)) (S m) (f n)) (S m).
-apply permut_S_to_permut.assumption.
-simplify.
-apply eqb_elim (f (S m)) (f (S m)).simplify.
-intro.reflexivity.
-intro.apply False_ind.apply H1.reflexivity.
-apply permut_transpose_l.
-unfold permut in H.
-elim H (S m).
-assumption.apply le_n.
-apply le_n.
-assumption.
+unfold permut.intros.
+elim H.
+split.intros.simplify.
+apply eqb_elim (f i) (f (S m)).simplify.
+intro.apply False_ind.
+cut i = (S m).
+apply not_le_Sn_n m.
+rewrite < Hcut.assumption.
+apply H2.apply le_S.assumption.apply le_n.assumption.
+intro.simplify.
+apply eqb_elim (f i) (S m).simplify.
+intro.
+cut f (S m) \lt (S m) \lor f (S m) = (S m).
+elim Hcut.apply le_S_S_to_le.assumption.
+apply False_ind.apply H4.rewrite > H6.assumption.
+apply le_to_or_lt_eq.apply H1.apply le_n.
+intro.simplify.
+cut f i \lt (S m) \lor f i = (S m).
+elim Hcut.apply le_S_S_to_le.assumption.
+apply False_ind.apply H5.assumption.
+apply le_to_or_lt_eq.apply H1.apply le_S.assumption.
+unfold injn.intros.
+apply H2.apply le_S.assumption.apply le_S.assumption.
+apply inj_transpose (f (S m)) (S m).
+apply H5.