+rewrite > (not_eq_to_eqb_false (f m) (f (S n1))).
+simplify.apply H2.
+apply injn_Sn_n. assumption.
+unfold Not.intro.absurd (m = S n1).
+apply H3.apply le_S.assumption.apply le_n.assumption.
+unfold Not.intro.
+apply (not_le_Sn_n n1).rewrite < H5.assumption.
+qed.
+
+theorem injective_invert_permut: \forall f:nat \to nat. \forall n:nat.
+permut f n \to injn (invert_permut n f) n.
+intros.
+unfold injn.intros.
+cut (bijn f n).
+unfold bijn in Hcut.
+generalize in match (Hcut i H1).intro.
+generalize in match (Hcut j H2).intro.
+elim H4.elim H6.
+elim H5.elim H9.
+rewrite < H8.
+rewrite < H11.
+apply eq_f.
+rewrite < (invert_permut_f f n a).
+rewrite < (invert_permut_f f n a1).
+rewrite > H8.
+rewrite > H11.
+assumption.assumption.
+unfold permut in H.elim H. assumption.
+assumption.
+unfold permut in H.elim H. assumption.
+apply permut_to_bijn.assumption.
+qed.
+
+theorem permut_invert_permut: \forall f:nat \to nat. \forall n:nat.
+permut f n \to permut (invert_permut n f) n.
+intros.unfold permut.split.
+intros.simplify.elim n.
+simplify.elim (eqb i (f O)).simplify.apply le_n.simplify.apply le_n.
+simplify.elim (eqb i (f (S n1))).simplify.apply le_n.
+simplify.apply le_S. assumption.
+apply injective_invert_permut.assumption.
+qed.
+
+theorem f_invert_permut: \forall f:nat \to nat. \forall n,m:nat.
+m \le n \to permut f n\to f (invert_permut n f m) = m.
+intros.
+apply (injective_invert_permut f n H1).
+unfold permut in H1.elim H1.
+apply H2.
+cut (permut (invert_permut n f) n).unfold permut in Hcut.
+elim Hcut.apply H4.assumption.
+apply permut_invert_permut.assumption.assumption.
+(* uffa: lo ha espanso troppo *)
+change with (invert_permut n f (f (invert_permut n f m)) = invert_permut n f m).
+apply invert_permut_f.
+cut (permut (invert_permut n f) n).unfold permut in Hcut.
+elim Hcut.apply H2.assumption.
+apply permut_invert_permut.assumption.
+unfold permut in H1.elim H1.assumption.
+qed.
+
+theorem permut_n_to_eq_n: \forall h:nat \to nat.\forall n:nat.
+permut h n \to (\forall m:nat. m < n \to h m = m) \to h n = n.
+intros.unfold permut in H.elim H.
+cut (invert_permut n h n < n \lor invert_permut n h n = n).
+elim Hcut.
+rewrite < (f_invert_permut h n n) in \vdash (? ? ? %).
+apply eq_f.
+rewrite < (f_invert_permut h n n) in \vdash (? ? % ?).
+apply H1.assumption.apply le_n.assumption.apply le_n.assumption.
+rewrite < H4 in \vdash (? ? % ?).
+apply (f_invert_permut h).apply le_n.assumption.
+apply le_to_or_lt_eq.
+cut (permut (invert_permut n h) n).
+unfold permut in Hcut.elim Hcut.
+apply H4.apply le_n.
+apply permut_invert_permut.assumption.
+qed.
+
+theorem permut_n_to_le: \forall h:nat \to nat.\forall k,n:nat.
+k \le n \to permut h n \to (\forall m:nat. m < k \to h m = m) \to
+\forall j. k \le j \to j \le n \to k \le h j.
+intros.unfold permut in H1.elim H1.
+cut (h j < k \lor \not(h j < k)).
+elim Hcut.absurd (k \le j).assumption.
+apply lt_to_not_le.
+cut (h j = j).rewrite < Hcut1.assumption.
+apply H6.apply H5.assumption.assumption.
+apply H2.assumption.
+apply not_lt_to_le.assumption.
+apply (decidable_lt (h j) k).