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