-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.
-