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. apply prc_comm_sv_left with (eq:=eq) (plus:=plus) (mult:=mult). apply eq_Equivalence. intros;ring. intros;ring. apply plus_morph. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)