[STATEMENT]
lemma mtx_vec_mult_minus_rdistrib: "(A - B) *\<^sub>V x = A *\<^sub>V x - B *\<^sub>V x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A - B) *\<^sub>V x = A *\<^sub>V x - B *\<^sub>V x
[PROOF STEP]
unfolding minus_sq_mtx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun to_vec (map_fun to_vec to_mtx) (-) A B *\<^sub>V x = A *\<^sub>V x - B *\<^sub>V x
[PROOF STEP]
by(transfer, simp add: matrix_vector_mult_diff_rdistrib)