1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/permutation".
17 include "nat/compare.ma".
18 include "nat/sigma_and_pi.ma".
20 definition permut : (nat \to nat) \to nat \to Prop
21 \def \lambda f:nat \to nat. \lambda m:nat.
22 \forall i:nat. i \le m \to (f i \le m \land
23 (\forall j:nat. f i = f j \to i = j)).
25 theorem permut_O_to_eq_O: \forall h:nat \to nat.
26 permut h O \to (h O) = O.
27 intros.unfold permut in H.
28 elim H O.apply sym_eq.apply le_n_O_to_eq.
29 assumption.apply le_n.
32 theorem permut_S_to_permut: \forall f:nat \to nat. \forall m:nat.
33 permut f (S m) \to f (S m) = (S m) \to permut f m.
37 cut f i < S m \lor f i = S m.
39 apply le_S_S_to_le.assumption.
43 rewrite > Hcut1.assumption.
44 apply H6.rewrite > H7.assumption.
45 apply le_to_or_lt_eq.assumption.
46 assumption.apply le_n.
47 apply le_S.assumption.
52 definition transpose : nat \to nat \to nat \to nat \def
59 | false \Rightarrow n]].
61 lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j.
62 intros.unfold transpose.
63 rewrite > eqb_n_n i.simplify. reflexivity.
66 lemma transpose_i_j_j: \forall i,j:nat. transpose i j j = i.
67 intros.unfold transpose.
68 apply eqb_elim j i.simplify.intro.assumption.
69 rewrite > eqb_n_n j.simplify.
73 theorem transpose_i_i: \forall i,n:nat. (transpose i i n) = n.
74 intros.unfold transpose.
76 intro.simplify.apply sym_eq. assumption.
77 intro.simplify.reflexivity.
80 theorem transpose_i_j_j_i: \forall i,j,n:nat.
81 transpose i j n = transpose j i n.
82 intros.unfold transpose.
85 intros. simplify.rewrite < H. rewrite < H1.
87 intros.simplify.reflexivity.
89 intros.simplify.reflexivity.
90 intros.simplify.reflexivity.
93 theorem transpose_transpose: \forall i,j,n:nat.
94 (transpose i j (transpose i j n)) = n.
95 intros.unfold transpose. unfold transpose.
96 apply eqb_elim n i.simplify.
99 simplify.intros.rewrite > H. rewrite > H1.reflexivity.
100 rewrite > eqb_n_n j.simplify.intros.
103 apply eqb_elim n j.simplify.
104 rewrite > eqb_n_n i.intros.simplify.
105 apply sym_eq. assumption.
107 rewrite > not_eq_to_eqb_false n i H1.
108 rewrite > not_eq_to_eqb_false n j H.
109 simplify.reflexivity.
112 theorem injective_transpose : \forall i,j:nat.
113 injective nat nat (transpose i j).
116 rewrite < transpose_transpose i j x.
117 rewrite < transpose_transpose i j y.
118 apply eq_f.assumption.
121 variant inj_transpose: \forall i,j,n,m:nat.
122 transpose i j n = transpose i j m \to n = m \def
125 theorem permut_transpose: \forall i,j,n:nat. i \le n \to j \le n \to
126 permut (transpose i j) n.
127 unfold permut.intros.
128 split.unfold transpose.
129 elim eqb i1 i.simplify.assumption.
130 elim eqb i1 j.simplify.assumption.
135 theorem permut_fg: \forall f,g:nat \to nat. \forall n:nat.
136 permut f n \to permut g n \to permut (\lambda m.(f(g m))) n.
137 unfold permut. intros.
138 split.simplify.elim H1 i.
139 elim H (g i).assumption.assumption.assumption.
140 intro.simplify.intros.
143 apply H7.assumption.assumption.assumption.
146 theorem permut_transpose_l:
147 \forall f:nat \to nat. \forall m,i,j:nat.
148 i \le m \to j \le m \to permut f m \to permut (\lambda n.transpose i j (f n)) m.
149 intros.apply permut_fg (transpose i j) f m ? ?.
150 apply permut_transpose.assumption.assumption.
154 theorem permut_transpose_r:
155 \forall f:nat \to nat. \forall m,i,j:nat.
156 i \le m \to j \le m \to permut f m \to permut (\lambda n.f (transpose i j n)) m.
157 intros.apply permut_fg f (transpose i j) m ? ?.
158 assumption.apply permut_transpose.assumption.assumption.
161 theorem eq_transpose : \forall i,j,k,n:nat. \lnot j=i \to
162 \lnot i=k \to \lnot j=k \to
163 transpose i j n = transpose i k (transpose k j (transpose i k n)).
164 (* uffa: triplo unfold? *)
165 intros.unfold transpose.unfold transpose.unfold transpose.
166 apply eqb_elim n i.intro.
167 simplify.rewrite > eqb_n_n k.
168 simplify.rewrite > not_eq_to_eqb_false j i H.
169 rewrite > not_eq_to_eqb_false j k H2.
171 intro.apply eqb_elim n j.
175 rewrite > not_eq_to_eqb_false n k Hcut.
177 rewrite > not_eq_to_eqb_false n k Hcut.
178 rewrite > eq_to_eqb_true n j H4.
180 rewrite > not_eq_to_eqb_false k i.
182 simplify.reflexivity.
183 simplify.intro.apply H1.apply sym_eq.assumption.
185 simplify.intro.apply H2.apply trans_eq ? ? n.
186 apply sym_eq.assumption.assumption.
187 intro.apply eqb_elim n k.intro.
189 rewrite > not_eq_to_eqb_false i k H1.
190 rewrite > not_eq_to_eqb_false i j.
194 simplify.intro.apply H.apply sym_eq.assumption.
196 rewrite > not_eq_to_eqb_false n k H5.
197 rewrite > not_eq_to_eqb_false n j H4.
199 rewrite > not_eq_to_eqb_false n i H3.
200 rewrite > not_eq_to_eqb_false n k H5.
201 simplify.reflexivity.
204 theorem permut_S_to_permut_transpose: \forall f:nat \to nat.
205 \forall m:nat. permut f (S m) \to permut (\lambda n.transpose (f (S m)) (S m)
208 cut permut (\lambda n.transpose (f (S m)) (S m) (f n)) (S m).
209 apply permut_S_to_permut.assumption.
211 apply eqb_elim (f (S m)) (f (S m)).simplify.
213 intro.apply False_ind.apply H1.reflexivity.
214 apply permut_transpose_l.
217 assumption.apply le_n.
222 (* bounded bijectivity *)
224 definition bijn : (nat \to nat) \to nat \to Prop \def
225 \lambda f:nat \to nat. \lambda n. \forall m:nat. m \le n \to
226 ex nat (\lambda p. p \le n \land f p = m).
228 theorem eq_to_bijn: \forall f,g:nat\to nat. \forall n:nat.
229 (\forall i:nat. i \le n \to (f i) = (g i)) \to
230 bijn f n \to bijn g n.
231 intros 4.unfold bijn.
233 apply ex_intro ? ? a.
234 rewrite < H a.assumption.
235 elim H3.assumption.assumption.
238 theorem bijn_Sn_n: \forall f:nat \to nat. \forall n:nat.
239 bijn f (S n) \to f (S n) = (S n) \to bijn f n.
240 unfold bijn.intros.elim H m.
242 apply ex_intro ? ? a.split.
243 cut a < S n \lor a = S n.
244 elim Hcut.apply le_S_S_to_le.assumption.
247 rewrite < H1.rewrite < H6.rewrite > H5.assumption.
248 apply le_to_or_lt_eq.assumption.assumption.
249 apply le_S.assumption.
252 theorem bijn_n_Sn: \forall f:nat \to nat. \forall n:nat.
253 bijn f n \to f (S n) = (S n) \to bijn f (S n).
255 cut m < S n \lor m = S n.
259 apply ex_intro ? ? a.split.
260 apply le_S.assumption.assumption.
261 apply le_S_S_to_le.assumption.
262 apply ex_intro ? ? (S n).
264 rewrite > H3.assumption.
265 apply le_to_or_lt_eq.assumption.
268 theorem bijn_fg: \forall f,g:nat\to nat. \forall n:nat.
269 bijn f n \to bijn g n \to bijn (\lambda p.f(g p)) n.
274 apply ex_intro ? ? a1.
276 rewrite > H8.assumption.
277 assumption.assumption.
280 theorem bijn_transpose : \forall n,i,j. i \le n \to j \le n \to
281 bijn (transpose i j) n.
282 intros.simplify.intros.
283 cut m = i \lor \lnot m = i.
285 apply ex_intro ? ? j.
288 intro.simplify.rewrite > H3.rewrite > H4.reflexivity.
289 rewrite > eqb_n_n j.simplify.
290 intros. apply sym_eq.assumption.
291 cut m = j \lor \lnot m = j.
293 apply ex_intro ? ? i.
295 rewrite > eqb_n_n i.simplify.
296 apply sym_eq. assumption.
297 apply ex_intro ? ? m.
299 rewrite > not_eq_to_eqb_false m i.
300 rewrite > not_eq_to_eqb_false m j.
301 simplify. reflexivity.
304 apply decidable_eq_nat m j.
305 apply decidable_eq_nat m i.
308 theorem bijn_transpose_r: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
309 bijn f n \to bijn (\lambda p.f (transpose i j p)) n.
311 apply bijn_fg f ?.assumption.
312 apply bijn_transpose n i j.assumption.assumption.
315 theorem bijn_transpose_l: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
316 bijn f n \to bijn (\lambda p.transpose i j (f p)) n.
319 apply bijn_transpose n i j.assumption.assumption.
324 theorem permut_to_bijn: \forall n:nat.\forall f:nat\to nat.
325 permut f n \to bijn f n.
327 elim n.simplify.intros.
328 apply ex_intro ? ? m.
330 apply le_n_O_elim m ? (\lambda p. f p = p).
332 elim H O.apply sym_eq. apply le_n_O_to_eq.assumption.
334 apply eq_to_bijn (\lambda p.
335 (transpose (f (S n1)) (S n1)) (transpose (f (S n1)) (S n1) (f p))) f.
336 intros.apply transpose_transpose.
337 apply bijn_fg (transpose (f (S n1)) (S n1)).
338 apply bijn_transpose.
340 elim H1 (S n1).assumption.apply le_n.apply le_n.
343 apply permut_S_to_permut_transpose.
345 rewrite > eqb_n_n (f (S n1)).simplify.reflexivity.
348 let rec invert_permut n f m \def
349 match eqb m (f n) with
354 |(S p) \Rightarrow invert_permut p f m]].
356 theorem invert_permut_f: \forall f:nat \to nat. \forall n,m:nat.
357 m \le n \to (\forall p:nat. f m = f p \to m = p) \to invert_permut n f (f m) = m.
362 rewrite > eqb_n_n (f O).simplify.reflexivity.
364 rewrite > eqb_n_n (f (S m1)).simplify.reflexivity.
366 rewrite > not_eq_to_eqb_false (f m) (f (S n1)).
367 simplify.apply H2.assumption.
368 simplify.intro.absurd m = S n1.
369 apply H3.assumption.simplify.intro.
370 apply not_le_Sn_n n1.rewrite < H5.assumption.
375 let rec map_iter n (g:nat \to nat) f (a:nat) \def
378 | (S p) \Rightarrow f (g p) (map_iter p g f a)].
380 theorem eq_map_iter: \forall g1,g2:nat \to nat.
381 \forall f:nat \to nat \to nat. \forall n,a:nat.
382 (\forall m:nat. m \lt n \to g1 m = g2 m) \to
383 map_iter n g1 f a = map_iter n g2 f a.
384 intros 5.elim n.simplify.reflexivity.
385 simplify.apply eq_f2.apply H1.simplify.apply le_n.
386 apply H.intros.apply H1.apply trans_lt ? n1.assumption.
390 (* map_iter examples *)
391 theorem eq_map_iter_sigma: \forall g:nat \to nat. \forall n:nat.
392 map_iter n g plus O = sigma n g.
393 intros.elim n.simplify.reflexivity.
395 apply eq_f.assumption.
398 theorem eq_map_iter_pi: \forall g:nat \to nat. \forall n:nat.
399 map_iter n g times (S O) = pi n g.
400 intros.elim n.simplify.reflexivity.
402 apply eq_f.assumption.
405 theorem eq_map_iter_transpose_i_Si : \forall f:nat\to nat \to nat.associative nat f \to
406 symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,i,a:nat. i \lt n \to
407 map_iter (S n) g f a = map_iter (S n) (\lambda m. g (transpose i (S i) m)) f a.
408 intros 5.elim n.apply False_ind.apply not_le_Sn_O i H2.
410 cut i < n1 \lor i = n1.
412 f (g (S n1)) (map_iter (S n1) g f a) =
413 f (g (transpose i (S i) (S n1))) (map_iter (S n1) (\lambda m. g (transpose i (S i) m)) f a).
415 cut g (transpose i (S i) (S n1)) = g (S n1).
417 rewrite < H2 i a H4.reflexivity.
419 rewrite > not_eq_to_eqb_false (S n1) i.
420 rewrite > not_eq_to_eqb_false (S n1) (S i).
421 simplify.reflexivity.
423 apply lt_to_not_eq i n1 H4.
424 apply injective_S i.apply sym_eq.assumption.
426 apply lt_to_not_eq i (S n1).
427 apply trans_lt ? n1.assumption.simplify.apply le_n.
428 apply sym_eq.assumption.
429 (* interesting case *)
431 change with f (g (S n1)) (f (g n1) (map_iter n1 g f a)) =
432 f (g (transpose n1 (S n1) (S n1)))
433 (f (g (transpose n1 (S n1) n1))
434 (map_iter n1 (\lambda m. g (transpose n1 (S n1) m)) f a)).
435 cut (g (transpose n1 (S n1) (S n1))) = g n1.
436 cut (g (transpose n1 (S n1) n1)) = g (S n1).
437 cut map_iter n1 (\lambda m. g (transpose n1 (S n1) m)) f a = map_iter n1 g f a.
438 rewrite > Hcut1.rewrite > Hcut2.rewrite > Hcut3.
440 rewrite > H1 (g (S n1)).
441 rewrite > H.reflexivity.
443 intros.unfold transpose.
444 rewrite > not_eq_to_eqb_false m n1.
445 rewrite > not_eq_to_eqb_false m (S n1).
446 simplify.reflexivity.
447 simplify. intro.apply lt_to_not_eq m (S n1).
448 apply trans_lt ? n1.assumption.simplify. apply le_n.
450 simplify. intro.apply lt_to_not_eq m n1.
451 assumption.assumption.
453 rewrite > eqb_n_n n1.simplify.reflexivity.
455 rewrite > not_eq_to_eqb_false.simplify.
456 rewrite > eqb_n_n n1.simplify.reflexivity.
458 apply not_eq_n_Sn n1. apply sym_eq.assumption.
459 apply le_to_or_lt_eq.
460 apply le_S_S_to_le.assumption.
463 theorem eq_map_iter_transpose: \forall f:nat\to nat \to nat.associative nat f \to
464 symmetric2 nat nat f \to \forall n,a,k:nat.
465 \forall g:nat \to nat. \forall i:nat. S (k + i) \le n \to
466 map_iter (S n) g f a = map_iter (S n) (\lambda m. g (transpose i (S(k + i)) m)) f a.
472 apply eq_map_iter_transpose_i_Si ? H H1.
475 apply trans_eq ? ? (map_iter (S n) (\lambda m. g (transpose i (S(m1 + i)) m)) f a).
477 simplify. apply le_n.
478 apply trans_le ? (S(S (m1+i))).
479 apply le_S.apply le_n.assumption.
480 apply trans_eq ? ? (map_iter (S n) (\lambda m. g
481 (transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f a).
482 apply H2 O ? ? (S(m1+i)).
483 simplify.apply le_S_S.apply le_O_n.
485 apply trans_eq ? ? (map_iter (S n) (\lambda m. g
486 (transpose i (S(m1 + i))
487 (transpose (S(m1 + i)) (S(S(m1 + i)))
488 (transpose i (S(m1 + i)) m)))) f a).
490 simplify. apply le_n.
491 apply trans_le ? (S(S (m1+i))).
492 apply le_S.apply le_n.assumption.
495 apply sym_eq. apply eq_transpose.
498 rewrite < H5 in \vdash (? ? %).
499 apply le_S_S.apply le_S.
503 rewrite > H5 in \vdash (? ? %).
507 apply not_eq_n_Sn (S m1+i).
508 apply sym_eq.assumption.
511 theorem eq_map_iter_transpose1: \forall f:nat\to nat \to nat.associative nat f \to
512 symmetric2 nat nat f \to \forall n,a,i,j:nat.
513 \forall g:nat \to nat. i < j \to j \le n \to
514 map_iter (S n) g f a = map_iter (S n) (\lambda m. g (transpose i j m)) f a.
517 cut (S i) < j \lor (S i) = j.
519 cut j = S ((j - (S i)) + i).
521 apply eq_map_iter_transpose f H H1 n a (j - (S i)) g i.
522 rewrite < Hcut1.assumption.
524 apply plus_minus_m_m.apply lt_to_le.assumption.
526 apply eq_map_iter_transpose_i_Si f H H1 g.
528 apply trans_le ? j.assumption.assumption.
529 apply le_to_or_lt_eq.assumption.
532 theorem eq_map_iter_transpose2: \forall f:nat\to nat \to nat.associative nat f \to
533 symmetric2 nat nat f \to \forall n,a,i,j:nat.
534 \forall g:nat \to nat. i \le n \to j \le n \to
535 map_iter (S n) g f a = map_iter (S n) (\lambda m. g (transpose i j m)) f a.
537 apply nat_compare_elim i j.
538 intro.apply eq_map_iter_transpose1 f H H1 n a i j g H4 H3.
540 apply eq_map_iter.intros.
541 rewrite > transpose_i_i j.reflexivity.
543 apply trans_eq ? ? (map_iter (S n) (\lambda m:nat.g (transpose j i m)) f a).
544 apply eq_map_iter_transpose1 f H H1 n a j i g H4 H2.
546 intros.apply eq_f.apply transpose_i_j_j_i.
549 theorem permut_to_eq_map_iter:\forall f:nat\to nat \to nat.associative nat f \to
550 symmetric2 nat nat f \to \forall a,n:nat.\forall g,h:nat \to nat.
552 map_iter (S n) g f a = map_iter (S n) (\lambda m.g(h m)) f a.
554 simplify.rewrite > permut_O_to_eq_O h.reflexivity.assumption.
555 apply trans_eq ? ? (map_iter (S(S n1)) (\lambda m.g ((transpose (h (S n1)) (S n1)) m)) f a).
556 apply eq_map_iter_transpose2 f H H1 (S n1) a ? ? g.
558 elim H3 (S n1).assumption.apply le_n.apply le_n.
559 apply trans_eq ? ? (map_iter (S(S n1)) (\lambda m.
560 (g(transpose (h (S n1)) (S n1)
561 (transpose (h (S n1)) (S n1) (h m)))) )f a).
563 f (g (transpose (h (S n1)) (S n1) (S n1)))
564 (map_iter (S n1) (\lambda m.
565 g (transpose (h (S n1)) (S n1) m)) f a)
568 (g(transpose (h (S n1)) (S n1)
569 (transpose (h (S n1)) (S n1) (h (S n1)))))
572 (g(transpose (h (S n1)) (S n1)
573 (transpose (h (S n1)) (S n1) (h m))))) f a).
574 apply eq_f2.apply eq_f.
575 rewrite > transpose_i_j_j.
576 rewrite > transpose_i_j_i.
577 rewrite > transpose_i_j_j.reflexivity.
578 apply H2 (\lambda m.(g(transpose (h (S n1)) (S n1) m))).
579 apply permut_S_to_permut_transpose.
581 apply eq_map_iter.intros.
582 rewrite > transpose_transpose.reflexivity.
585 theorem eq_sigma_transpose_i_Si: \forall n,i:nat. \forall f:nat \to nat. i \lt n \to
586 sigma (S n) f = sigma (S n) (\lambda m. f (transpose i (S i) m)).
587 intro.elim n.apply False_ind.apply not_le_Sn_O i H.
589 cut i < n1 \lor i = n1.
591 (f (S n1))+(sigma (S n1) f) =
592 (f (transpose i (S i) (S n1)))+(sigma (S n1) (\lambda m. f (transpose i (S i) m))).
594 cut f (transpose i (S i) (S n1)) = f (S n1).
596 rewrite < H i f.reflexivity.
597 assumption.unfold transpose.
598 rewrite > not_eq_to_eqb_false (S n1) i.
599 rewrite > not_eq_to_eqb_false (S n1) (S i).
600 simplify.reflexivity.
602 apply lt_to_not_eq i n1 H2.
603 apply injective_S i.apply sym_eq.assumption.
605 apply lt_to_not_eq i (S n1).
606 apply trans_lt ? n1.assumption.simplify.apply le_n.
607 apply sym_eq.assumption.
609 change with (f (S n1))+((f n1)+(sigma n1 f)) =
610 (f (transpose n1 (S n1) (S n1)))+
611 ((f (transpose n1 (S n1) n1))+
612 (sigma n1 (\lambda m. f (transpose n1 (S n1) m)))).
613 cut (f (transpose n1 (S n1) (S n1))) = f n1.
614 cut (f (transpose n1 (S n1) n1)) = f (S n1).
615 cut sigma n1 (\lambda m. f (transpose n1 (S n1) m)) = sigma n1 f.
616 rewrite > Hcut1.rewrite > Hcut2.rewrite > Hcut3.
617 rewrite < assoc_plus.rewrite > sym_plus (f (S n1)).
618 rewrite > assoc_plus.reflexivity.
620 intros.unfold transpose.
621 rewrite > not_eq_to_eqb_false m n1.
622 rewrite > not_eq_to_eqb_false m (S n1).
623 simplify.reflexivity.
624 simplify. intro.apply lt_to_not_eq m (S n1).
625 apply trans_lt ? n1.assumption.simplify. apply le_n.
627 simplify. intro.apply lt_to_not_eq m n1.
628 assumption.assumption.
630 rewrite > eqb_n_n n1.simplify.reflexivity.
632 rewrite > not_eq_to_eqb_false.simplify.
633 rewrite > eqb_n_n n1.simplify.reflexivity.
635 apply not_eq_n_Sn n1. apply sym_eq.assumption.
636 apply le_to_or_lt_eq.
637 apply le_S_S_to_le.assumption.
640 theorem eq_sigma_transpose: \forall n,k:nat. \forall f:nat \to nat.
641 \forall i. S (k + i) \le n \to
642 sigma (S n) f = sigma (S n) (\lambda m. f (transpose i (S(k + i)) m)).
648 apply eq_sigma_transpose_i_Si n i f.
651 apply trans_eq ? ? (sigma (S n) (\lambda m. f (transpose i (S(m1 + i)) m))).
653 simplify. apply le_n.
654 apply trans_le ? (S(S (m1+i))).
655 apply le_S.apply le_n.assumption.
656 apply trans_eq ? ? (sigma (S n) (\lambda m. f
657 (transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m)))).
658 apply H O ? ? (S(m1+i)) ?.
659 simplify.apply le_S_S.apply le_O_n.
661 apply trans_eq ? ? (sigma (S n) (\lambda m. f
662 (transpose i (S(m1 + i))
663 (transpose (S(m1 + i)) (S(S(m1 + i)))
664 (transpose i (S(m1 + i)) m))))).
666 simplify. apply le_n.
667 apply trans_le ? (S(S (m1+i))).
668 apply le_S.apply le_n.assumption.
671 apply sym_eq. apply eq_transpose.
674 rewrite < H3 in \vdash (? ? %).
675 apply le_S_S.apply le_S.
679 rewrite > H3 in \vdash (? ? %).
683 apply not_eq_n_Sn (S m1+i).
684 apply sym_eq.assumption.
688 theorem bad: \forall n:nat. \forall f:nat \to nat.
689 permut f n \to sigma (S n) f = sigma (S n) (\lambda n.n).
691 simplify.unfold permut in H.elim H O.
692 rewrite < (le_n_O_to_eq (f O)).simplify. reflexivity.apply le_n.
693 cut permut (\lambda n.transpose (f (S n1)) (S n1) (f n)) n1.
695 (sigma (S(S n1)) (\lambda n.transpose (f (S n1)) (S n1) (f n))).