+lemma change_vec_commute : ∀A,n,v,a,b,i,j. i ≠ j →
+ change_vec A n (change_vec A n v a i) b j
+ = change_vec A n (change_vec A n v b j) a i.
+#A #n #v #a #b #i #j #Hij @(eq_vec … a)
+#k #Hk cases (decidable_eq_nat k i) #Hki
+[ >Hki >nth_change_vec // >(nth_change_vec_neq ??????? (sym_not_eq … Hij))
+ >nth_change_vec //
+| cases (decidable_eq_nat k j) #Hkj
+ [ >Hkj >nth_change_vec // >(nth_change_vec_neq ??????? Hij) >nth_change_vec //
+ | >(nth_change_vec_neq ??????? (sym_not_eq … Hki))
+ >(nth_change_vec_neq ??????? (sym_not_eq … Hkj))
+ >(nth_change_vec_neq ??????? (sym_not_eq … Hki))
+ >(nth_change_vec_neq ??????? (sym_not_eq … Hkj)) //
+ ]
+]
+qed.
+
+lemma change_vec_change_vec : ∀A,n,v,a,b,i.
+ change_vec A n (change_vec A n v a i) b i = change_vec A n v b i.
+#A #n #v #a #b #i @(eq_vec … a) #i0 #Hi0
+cases (decidable_eq_nat i i0) #Hii0
+[ >Hii0 >nth_change_vec // >nth_change_vec //
+| >nth_change_vec_neq // >nth_change_vec_neq //
+ >nth_change_vec_neq // ]
+qed.
+
+