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/library_autobatch/nat/permutation".
17 include "auto/nat/compare.ma".
18 include "auto/nat/sigma_and_pi.ma".
20 definition injn: (nat \to nat) \to nat \to Prop \def
21 \lambda f:nat \to nat.\lambda n:nat.\forall i,j:nat.
22 i \le n \to j \le n \to f i = f j \to i = j.
24 theorem injn_Sn_n: \forall f:nat \to nat. \forall n:nat.
25 injn f (S n) \to injn f n.
37 theorem injective_to_injn: \forall f:nat \to nat. \forall n:nat.
38 injective nat nat f \to injn f n.
46 definition permut : (nat \to nat) \to nat \to Prop
47 \def \lambda f:nat \to nat. \lambda m:nat.
48 (\forall i:nat. i \le m \to f i \le m )\land injn f m.
50 theorem permut_O_to_eq_O: \forall h:nat \to nat.
51 permut h O \to (h O) = O.
55 apply sym_eq.autobatch.
61 theorem permut_S_to_permut: \forall f:nat \to nat. \forall m:nat.
62 permut f (S m) \to f (S m) = (S m) \to permut f m.
68 cut (f i < S m \lor f i = S m)
74 apply (not_le_Sn_n m).
89 | apply le_to_or_lt_eq.
95 | apply (injn_Sn_n f m H3)
101 definition transpose : nat \to nat \to nat \to nat \def
108 | false \Rightarrow n]].
110 notation < "(❲i↹j❳)n"
111 right associative with precedence 71
112 for @{ 'transposition $i $j $n}.
114 notation < "(❲i \atop j❳)n"
115 right associative with precedence 71
116 for @{ 'transposition $i $j $n}.
118 interpretation "natural transposition" 'transposition i j n =
119 (cic:/matita/library_autobatch/nat/permutation/transpose.con i j n).
121 lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j.
124 (*dopo circa 6 minuti, l'esecuzione di autobatch in questo punto non era ancora terminata*)
125 rewrite > (eqb_n_n i).autobatch.
130 lemma transpose_i_j_j: \forall i,j:nat. transpose i j j = i.
138 | rewrite > (eqb_n_n j).
145 theorem transpose_i_i: \forall i,n:nat. (transpose i i n) = n.
161 theorem transpose_i_j_j_i: \forall i,j,n:nat.
162 transpose i j n = transpose j i n.
166 [ apply (eqb_elim n j)
168 (*l'esecuzione di autobatch in questo punto, dopo circa 300 secondi, non era ancora terminata*)
178 | apply (eqb_elim n j)
180 (*simplify.reflexivity *)
182 (*simplify.reflexivity*)
187 theorem transpose_transpose: \forall i,j,n:nat.
188 (transpose i j (transpose i j n)) = n.
202 | rewrite > (eqb_n_n j).
209 | apply (eqb_elim n j)
211 rewrite > (eqb_n_n i).
219 (*l'esecuzione di autobatch in questo punto, dopo piu' di 6 minuti non era ancora terminata*)
220 rewrite > (not_eq_to_eqb_false n i H1).
221 (*l'esecuzione di autobatch in questo punto, dopo piu' alcuni minuti non era ancora terminata*)
222 rewrite > (not_eq_to_eqb_false n j H).autobatch
229 theorem injective_transpose : \forall i,j:nat.
230 injective nat nat (transpose i j).
233 (*rewrite < (transpose_transpose i j x).
234 rewrite < (transpose_transpose i j y).
239 variant inj_transpose: \forall i,j,n,m:nat.
240 transpose i j n = transpose i j m \to n = m \def
243 theorem permut_transpose: \forall i,j,n:nat. i \le n \to j \le n \to
244 permut (transpose i j) n.
251 [ (*qui autobatch non chiude il goal*)
255 [ (*aui autobatch non chiude il goal*)
258 | (*aui autobatch non chiude il goal*)
264 (*apply (injective_to_injn (transpose i j) n).
265 apply injective_transpose*)
269 theorem permut_fg: \forall f,g:nat \to nat. \forall n:nat.
270 permut f n \to permut g n \to permut (\lambda m.(f(g m))) n.
300 theorem permut_transpose_l:
301 \forall f:nat \to nat. \forall m,i,j:nat.
302 i \le m \to j \le m \to permut f m \to permut (\lambda n.transpose i j (f n)) m.
305 (*apply (permut_fg (transpose i j) f m ? ?)
306 [ apply permut_transpose;assumption
311 theorem permut_transpose_r:
312 \forall f:nat \to nat. \forall m,i,j:nat.
313 i \le m \to j \le m \to permut f m \to permut (\lambda n.f (transpose i j n)) m.
315 (*apply (permut_fg f (transpose i j) m ? ?)
317 | apply permut_transpose;assumption
321 theorem eq_transpose : \forall i,j,k,n:nat. \lnot j=i \to
322 \lnot i=k \to \lnot j=k \to
323 transpose i j n = transpose i k (transpose k j (transpose i k n)).
324 (* uffa: triplo unfold? *)
325 intros.unfold transpose.
331 rewrite > (eqb_n_n k).
333 rewrite > (not_eq_to_eqb_false j i H).
334 rewrite > (not_eq_to_eqb_false j k H2).
341 [ rewrite > (not_eq_to_eqb_false n k Hcut).
343 rewrite > (not_eq_to_eqb_false n k Hcut).
344 rewrite > (eq_to_eqb_true n j H4).
346 rewrite > (not_eq_to_eqb_false k i)
347 [ rewrite > (eqb_n_n k).
362 apply (trans_eq ? ? n)
372 rewrite > (not_eq_to_eqb_false i k H1).
373 rewrite > (not_eq_to_eqb_false i j)
375 rewrite > (eqb_n_n i).
387 rewrite > (not_eq_to_eqb_false n k H5).
388 rewrite > (not_eq_to_eqb_false n j H4).
390 rewrite > (not_eq_to_eqb_false n i H3).
391 rewrite > (not_eq_to_eqb_false n k H5).
400 theorem permut_S_to_permut_transpose: \forall f:nat \to nat.
401 \forall m:nat. permut f (S m) \to permut (\lambda n.transpose (f (S m)) (S m)
410 apply (eqb_elim (f i) (f (S m)))
414 [ apply (not_le_Sn_n m).
426 apply (eqb_elim (f i) (S m))
428 cut (f (S m) \lt (S m) \lor f (S m) = (S m))
430 [ apply le_S_S_to_le.
431 (*NB qui autobatch non chiude il goal*)
440 (*apply le_to_or_lt_eq.
445 cut (f i \lt (S m) \lor f i = (S m))
448 (*apply le_S_S_to_le.
455 | apply le_to_or_lt_eq.
470 | apply (inj_transpose (f (S m)) (S m)).
476 (* bounded bijectivity *)
478 definition bijn : (nat \to nat) \to nat \to Prop \def
479 \lambda f:nat \to nat. \lambda n. \forall m:nat. m \le n \to
480 ex nat (\lambda p. p \le n \land f p = m).
482 theorem eq_to_bijn: \forall f,g:nat\to nat. \forall n:nat.
483 (\forall i:nat. i \le n \to (f i) = (g i)) \to
484 bijn f n \to bijn g n.
489 [ apply (ex_intro ? ? a).
499 theorem bijn_Sn_n: \forall f:nat \to nat. \forall n:nat.
500 bijn f (S n) \to f (S n) = (S n) \to bijn f n.
505 apply (ex_intro ? ? a).
507 [ cut (a < S n \lor a = S n)
510 (*apply le_S_S_to_le.
513 apply (not_le_Sn_n n).
520 (*apply le_to_or_lt_eq.
531 theorem bijn_n_Sn: \forall f:nat \to nat. \forall n:nat.
532 bijn f n \to f (S n) = (S n) \to bijn f (S n).
535 cut (m < S n \lor m = S n)
539 apply (ex_intro ? ? a).
547 (*apply le_S_S_to_le.
551 (*apply (ex_intro ? ? (S n)).
559 (*apply le_to_or_lt_eq.
564 theorem bijn_fg: \forall f,g:nat\to nat. \forall n:nat.
565 bijn f n \to bijn g n \to bijn (\lambda p.f(g p)) n.
574 (*apply (ex_intro ? ? a1).
586 theorem bijn_transpose : \forall n,i,j. i \le n \to j \le n \to
587 bijn (transpose i j) n.
592 cut (m = i \lor \lnot m = i)
594 [ apply (ex_intro ? ? j).
597 | apply (eqb_elim j i)
599 (*dopo circa 360 secondi l'esecuzione di autobatch in questo punto non era ancora terminata*)
605 | rewrite > (eqb_n_n j).
613 | cut (m = j \lor \lnot m = j)
615 [ apply (ex_intro ? ? i).
618 | (*dopo circa 5 minuti, l'esecuzione di autobatch in questo punto non era ancora terminata*)
619 rewrite > (eqb_n_n i).
625 | apply (ex_intro ? ? m).
628 | rewrite > (not_eq_to_eqb_false m i)
629 [ (*dopo circa 5 minuti, l'esecuzione di autobatch in questo punto non era ancora terminata*)
630 rewrite > (not_eq_to_eqb_false m j)
640 | apply (decidable_eq_nat m j)
643 | apply (decidable_eq_nat m i)
647 theorem bijn_transpose_r: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
648 bijn f n \to bijn (\lambda p.f (transpose i j p)) n.
650 (*apply (bijn_fg f ?)
652 | apply (bijn_transpose n i j)
659 theorem bijn_transpose_l: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
660 bijn f n \to bijn (\lambda p.transpose i j (f p)) n.
663 (*apply (bijn_fg ? f)
664 [ apply (bijn_transpose n i j)
672 theorem permut_to_bijn: \forall n:nat.\forall f:nat\to nat.
673 permut f n \to bijn f n.
678 apply (ex_intro ? ? m).
681 | apply (le_n_O_elim m ? (\lambda p. f p = p))
683 | unfold permut in H.
687 (*apply le_n_O_to_eq.
692 | apply (eq_to_bijn (\lambda p.
693 (transpose (f (S n1)) (S n1)) (transpose (f (S n1)) (S n1) (f p))) f)
695 apply transpose_transpose
696 | apply (bijn_fg (transpose (f (S n1)) (S n1)))
697 [ apply bijn_transpose
698 [ unfold permut in H1.
707 (*apply permut_S_to_permut_transpose.
711 rewrite > (eqb_n_n (f (S n1))).
720 let rec invert_permut n f m \def
721 match eqb m (f n) with
726 |(S p) \Rightarrow invert_permut p f m]].
728 theorem invert_permut_f: \forall f:nat \to nat. \forall n,m:nat.
729 m \le n \to injn f n\to invert_permut n f (f m) = m.
732 [ apply (nat_case1 m)
735 (*l'applicazione di autobatch in questo punto, dopo alcuni minuti, non aveva ancora dato risultati*)
736 rewrite > (eqb_n_n (f O)).
741 (*l'applicazione di autobatch in questo punto, dopo alcuni minuti, non aveva ancora dato risultati*)
742 rewrite > (eqb_n_n (f (S m1))).
748 rewrite > (not_eq_to_eqb_false (f m) (f (S n1)))
749 [ (*l'applicazione di autobatch in questo punto, dopo parecchi secondi, non aveva ancora prodotto un risultato*)
766 apply (not_le_Sn_n n1).
774 theorem injective_invert_permut: \forall f:nat \to nat. \forall n:nat.
775 permut f n \to injn (invert_permut n f) n.
780 [ unfold bijn in Hcut.
781 generalize in match (Hcut i H1).
783 generalize in match (Hcut j H2).
792 rewrite < (invert_permut_f f n a)
793 [ rewrite < (invert_permut_f f n a1)
798 | unfold permut in H.elim H.
802 | unfold permut in H.
807 (*apply permut_to_bijn.
812 theorem permut_invert_permut: \forall f:nat \to nat. \forall n:nat.
813 permut f n \to permut (invert_permut n f) n.
821 elim (eqb i (f O));autobatch
828 elim (eqb i (f (S n1)))
839 (*apply injective_invert_permut.
844 theorem f_invert_permut: \forall f:nat \to nat. \forall n,m:nat.
845 m \le n \to permut f n\to f (invert_permut n f m) = m.
847 apply (injective_invert_permut f n H1)
848 [ unfold permut in H1.
851 cut (permut (invert_permut n f) n)
852 [ unfold permut in Hcut.
856 | apply permut_invert_permut.
857 (*NB qui autobatch non chiude il goal*)
861 | apply invert_permut_f
862 [ cut (permut (invert_permut n f) n)
863 [ unfold permut in Hcut.
869 (*apply permut_invert_permut.
872 | unfold permut in H1.
879 theorem permut_n_to_eq_n: \forall h:nat \to nat.\forall n:nat.
880 permut h n \to (\forall m:nat. m < n \to h m = m) \to h n = n.
884 cut (invert_permut n h n < n \lor invert_permut n h n = n)
886 [ rewrite < (f_invert_permut h n n) in \vdash (? ? ? %)
888 rewrite < (f_invert_permut h n n) in \vdash (? ? % ?)
893 | (*qui autobatch NON chiude il goal*)
897 | (*qui autobatch NON chiude il goal*)
900 | rewrite < H4 in \vdash (? ? % ?).
901 apply (f_invert_permut h)
903 | (*qui autobatch NON chiude il goal*)
907 | apply le_to_or_lt_eq.
908 cut (permut (invert_permut n h) n)
909 [ unfold permut in Hcut.
914 | apply permut_invert_permut.
915 (*NB aui autobatch non chiude il goal*)
921 theorem permut_n_to_le: \forall h:nat \to nat.\forall k,n:nat.
922 k \le n \to permut h n \to (\forall m:nat. m < k \to h m = m) \to
923 \forall j. k \le j \to j \le n \to k \le h j.
927 cut (h j < k \lor \not(h j < k))
931 | apply lt_to_not_le.
945 (*apply not_lt_to_le.
948 | apply (decidable_lt (h j) k)
954 let rec map_iter_i k (g:nat \to nat) f (i:nat) \def
957 | (S k) \Rightarrow f (g (S (k+i))) (map_iter_i k g f i)].
959 theorem eq_map_iter_i: \forall g1,g2:nat \to nat.
960 \forall f:nat \to nat \to nat. \forall n,i:nat.
961 (\forall m:nat. i\le m \to m \le n+i \to g1 m = g2 m) \to
962 map_iter_i n g1 f i = map_iter_i n g2 f i.
993 (* map_iter examples *)
995 theorem eq_map_iter_i_sigma: \forall g:nat \to nat. \forall n,m:nat.
996 map_iter_i n g plus m = sigma n g m.
1009 theorem eq_map_iter_i_pi: \forall g:nat \to nat. \forall n,m:nat.
1010 map_iter_i n g times m = pi n g m.
1023 theorem eq_map_iter_i_fact: \forall n:nat.
1024 map_iter_i n (\lambda m.m) times (S O) = (S n)!.
1031 (((S n1)+(S O))*(map_iter_i n1 (\lambda m.m) times (S O)) = (S(S n1))*(S n1)!).
1032 rewrite < plus_n_Sm.
1035 (*NB: qui autobatch non chiude il goal!!!*)
1041 theorem eq_map_iter_i_transpose_l : \forall f:nat\to nat \to nat.associative nat f \to
1042 symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k:nat.
1043 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose (k+n) (S k+n) m)) f n.
1048 fold simplify (transpose n (S n) (S n)).
1050 (*rewrite > transpose_i_j_i.
1051 rewrite > transpose_i_j_j.
1055 (f (g (S (S (m+n)))) (f (g (S (m+n))) (map_iter_i m g f n)) =
1056 f (g (transpose (S m + n) (S (S m) + n) (S (S m)+n)))
1057 (f (g (transpose (S m + n) (S (S m) + n) (S m+n)))
1058 (map_iter_i m (\lambda m1. g (transpose (S m+n) (S (S m)+n) m1)) f n))).
1059 rewrite > transpose_i_j_i.
1060 rewrite > transpose_i_j_j.
1063 rewrite < (H1 (g (S m + n))).
1065 apply eq_map_iter_i.
1069 rewrite > (not_eq_to_eqb_false m1 (S m+n))
1070 [ rewrite > (not_eq_to_eqb_false m1 (S (S m)+n))
1074 | apply (lt_to_not_eq m1 (S ((S m)+n))).
1078 change with (m1 \leq S (m+n)).
1082 | apply (lt_to_not_eq m1 (S m+n)).
1091 theorem eq_map_iter_i_transpose_i_Si : \forall f:nat\to nat \to nat.associative nat f \to
1092 symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k,i:nat. n \le i \to i \le k+n \to
1093 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S i) m)) f n.
1098 (*qui autobatch non chiude il goal*)
1099 apply (eq_map_iter_i_transpose_l f H H1 g n O)
1100 | apply antisymmetric_le
1105 | cut (i < S n1 + n \lor i = S n1 + n)
1108 (f (g (S (S n1)+n)) (map_iter_i (S n1) g f n) =
1109 f (g (transpose i (S i) (S (S n1)+n))) (map_iter_i (S n1) (\lambda m. g (transpose i (S i) m)) f n)).
1112 rewrite > (not_eq_to_eqb_false (S (S n1)+n) i)
1113 [ rewrite > (not_eq_to_eqb_false (S (S n1)+n) (S i))
1120 apply (lt_to_not_eq i (S n1+n))
1131 apply (lt_to_not_eq i (S (S n1+n)))
1142 | apply H2;autobatch
1144 | apply le_S_S_to_le.
1149 (*qui autobatch non chiude il goal*)
1150 apply (eq_map_iter_i_transpose_l f H H1 g n (S n1)).
1153 (*apply le_to_or_lt_eq.
1159 theorem eq_map_iter_i_transpose:
1160 \forall f:nat\to nat \to nat.
1161 associative nat f \to symmetric2 nat nat f \to \forall n,k,o:nat.
1162 \forall g:nat \to nat. \forall i:nat. n \le i \to S (o + i) \le S k+n \to
1163 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S(o + i)) m)) f n.
1165 apply (nat_elim1 o).
1167 apply (nat_case m ?)
1169 apply (eq_map_iter_i_transpose_i_Si ? H H1);autobatch
1171 | apply le_S_S_to_le.
1175 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n))
1181 | apply (trans_le ? (S(S (m1+i))))
1185 | (*qui autobatch non chiude il goal, chiuso invece da assumption*)
1189 | apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
1190 (transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n))
1191 [ (*qui autobatch dopo alcuni minuti non aveva ancora terminato la propria esecuzione*)
1192 apply (H2 O ? ? (S(m1+i)))
1198 (*apply (trans_le ? i)
1200 | change with (i \le (S m1)+i).
1203 | (*qui autobatch non chiude il goal*)
1206 | apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
1207 (transpose i (S(m1 + i))
1208 (transpose (S(m1 + i)) (S(S(m1 + i)))
1209 (transpose i (S(m1 + i)) m)))) f n))
1210 [ (*qui autobatch dopo alcuni minuti non aveva ancora terminato la propria esecuzione*)
1216 | apply (trans_le ? (S(S (m1+i))))
1220 | (*qui autobatch NON CHIUDE il goal*)
1224 | apply eq_map_iter_i.
1231 apply (not_le_Sn_n i).
1232 rewrite < H7 in \vdash (? ? %).
1239 apply (not_le_Sn_n i).
1240 rewrite > H7 in \vdash (? ? %).
1247 (*apply (not_eq_n_Sn (S m1+i)).
1257 theorem eq_map_iter_i_transpose1: \forall f:nat\to nat \to nat.associative nat f \to
1258 symmetric2 nat nat f \to \forall n,k,i,j:nat.
1259 \forall g:nat \to nat. n \le i \to i < j \to j \le S k+n \to
1260 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
1263 cut ((S i) < j \lor (S i) = j)
1265 [ cut (j = S ((j - (S i)) + i))
1267 apply (eq_map_iter_i_transpose f H H1 n k (j - (S i)) g i)
1272 | rewrite > plus_n_Sm.
1274 (*apply plus_minus_m_m.
1279 apply (eq_map_iter_i_transpose_i_Si f H H1 g)
1283 | apply le_S_S_to_le.
1285 (*apply (trans_le ? j)
1292 (*apply le_to_or_lt_eq.
1297 theorem eq_map_iter_i_transpose2: \forall f:nat\to nat \to nat.associative nat f \to
1298 symmetric2 nat nat f \to \forall n,k,i,j:nat.
1299 \forall g:nat \to nat. n \le i \to i \le (S k+n) \to n \le j \to j \le (S k+n) \to
1300 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
1302 apply (nat_compare_elim i j)
1304 (*qui autobatch non chiude il goal*)
1305 apply (eq_map_iter_i_transpose1 f H H1 n k i j g H2 H6 H5)
1308 apply eq_map_iter_i.
1311 (*rewrite > (transpose_i_i j).
1314 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m:nat.g (transpose j i m)) f n))
1315 [ apply (eq_map_iter_i_transpose1 f H H1 n k j i g H4 H6 H3)
1316 | apply eq_map_iter_i.
1320 apply transpose_i_j_j_i*)
1325 theorem permut_to_eq_map_iter_i:\forall f:nat\to nat \to nat.associative nat f \to
1326 symmetric2 nat nat f \to \forall k,n:nat.\forall g,h:nat \to nat.
1327 permut h (k+n) \to (\forall m:nat. m \lt n \to h m = m) \to
1328 map_iter_i k g f n = map_iter_i k (\lambda m.g(h m)) f n.
1332 rewrite > (permut_n_to_eq_n h)
1334 | (*qui autobatch non chiude il goal*)
1336 | (*qui autobatch non chiude il goal*)
1339 | apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.g ((transpose (h (S n+n1)) (S n+n1)) m)) f n1))
1340 [ unfold permut in H3.
1342 apply (eq_map_iter_i_transpose2 f H H1 n1 n ? ? g)
1343 [ apply (permut_n_to_le h n1 (S n+n1))
1345 | (*qui autobatch non chiude il goal*)
1347 | (*qui autobatch non chiude il goal*)
1358 | apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.
1359 (g(transpose (h (S n+n1)) (S n+n1)
1360 (transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1))
1362 fold simplify (transpose (h (S n+n1)) (S n+n1) (S n+n1)).
1366 rewrite > transpose_i_j_j.
1367 rewrite > transpose_i_j_i.
1368 rewrite > transpose_i_j_j.
1370 | apply (H2 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m))))
1371 [ apply permut_S_to_permut_transpose.
1372 (*qui autobatch non chiude il goal*)
1376 rewrite > (not_eq_to_eqb_false (h m) (h (S n+n1)))
1377 [ rewrite > (not_eq_to_eqb_false (h m) (S n+n1))
1384 (*apply lt_to_not_eq.
1385 apply (trans_lt ? n1)
1395 | unfold permut in H3.
1400 apply (lt_to_not_eq m (S n+n1))
1402 (*apply (trans_lt ? n1)
1409 | unfold injn in H7.
1410 apply (H7 m (S n+n1))
1412 (*apply (trans_le ? n1)
1424 | apply eq_map_iter_i.
1427 (*rewrite > transpose_transpose.