proposition: Lemma prc_comm_sv_left : forall dim (r c : vector dim) (a:A), prod_row_col _ (prod_scal_vec _ a r) c == mult a (prod_row_col _ r c).
proof: Proof. fix prc_comm_sv_left 1. intros [|dim]. simpl. intros;apply mult_assoc. simpl vector. intros [a1 r1] [a2 c2] a. simpl. rewrite prc_comm_sv_left. rewrite mult_distrib_right. rewrite mult_assoc. reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)