+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.
+qed.
+