...

[helm.git] / matita / library / nat / permutation.ma

diff --git a/matita/library/nat/permutation.ma b/matita/library/nat/permutation.ma
index d71f4fd27a2690b14358c9fb035ef83cdb451b55..768e0bd6091c50c0b4bc93ff767b4820e978c2c3 100644 (file)
--- a/matita/library/nat/permutation.ma
+++ b/matita/library/nat/permutation.ma
@@ -73,7 +73,18 @@ match eqb n i with
       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.
@@ -530,10 +541,7 @@ theorem eq_map_iter_i_transpose_l : \forall f:nat\to nat \to nat.associative nat
 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.
@@ -698,18 +706,7 @@ apply H5.apply le_n.apply le_plus_n.apply le_n.
 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.