match eqb n j with
[ true \Rightarrow i
| false \Rightarrow n]].
-
+
+notation < "(❲i↹j❳)n"
+ right associative with precedence 71
+for @{ 'transposition $i $j $n}.
+
+notation < "(❲i \atop j❳)n"
+ right associative with precedence 71
+for @{ 'transposition $i $j $n}.
+
+interpretation "natural transposition" 'transposition i j n =
+ (cic:/matita/nat/permutation/transpose.con i j n).
+
lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j.
intros.unfold transpose.
rewrite > (eqb_n_n i).simplify. reflexivity.
symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k:nat.
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.
intros.apply (nat_case1 k).
-intros.simplify.
-change with
-(f (g (S n)) (g n) =
-f (g (transpose n (S n) (S n))) (g (transpose n (S n) n))).
+intros.simplify.fold simplify (transpose n (S n) (S n)).
rewrite > transpose_i_j_i.
rewrite > transpose_i_j_j.
apply H1.
apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.
(g(transpose (h (S n+n1)) (S n+n1)
(transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1)).
-change with
-(f (g (transpose (h (S n+n1)) (S n+n1) (S n+n1)))
-(map_iter_i n (\lambda m.
-g (transpose (h (S n+n1)) (S n+n1) m)) f n1)
-=
-f
-(g(transpose (h (S n+n1)) (S n+n1)
-(transpose (h (S n+n1)) (S n+n1) (h (S n+n1)))))
-(map_iter_i n
-(\lambda m.
-(g(transpose (h (S n+n1)) (S n+n1)
-(transpose (h (S n+n1)) (S n+n1) (h m))))) f n1)).
+simplify.fold simplify (transpose (h (S n+n1)) (S n+n1) (S n+n1)).
apply eq_f2.apply eq_f.
rewrite > transpose_i_j_j.
rewrite > transpose_i_j_i.