proposition: Lemma pm_comm_sv_right : forall dim (m1 m2:matrix dim) (a:A), prod_matrix _ (prod_scal_mat _ a m1) m2 ==m prod_scal_mat _ a (prod_matrix _ m1 m2).
proof: Proof. fix pm_comm_sv_right 1. intros [|dim]. simpl. intros;apply mult_assoc. simpl vector;simpl matrix. intros [a1 [r1 [c1 m1]]] [a2 [r2 [c2 m2]]] a. simpl. refine (conj _ (conj _ (conj _ _ ))). repeat rewrite mult_distrib_right. rewrite mult_assoc. rewrite prc_comm_sv_left. reflexivity. repeat rewrite psv_distrib_right. rewrite <- psv_assoc. rewrite prm_comm_sv_left. reflexivity. repeat rewrite psv_distrib_right. rewrite psv_comm. rewrite pmc_comm_sv_left. reflexivity. repeat rewrite psm_distrib_right. rewrite pcr_comm_sv_left. rewrite pm_comm_sv_right. reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)