proposition: Lemma pcr_comm_sv_right : forall dim (c r : vector dim) (a:A), prod_col_row _ c (prod_scal_vec _ a r) ==m prod_scal_mat _ a (prod_col_row _ c r).
proof: Proof. apply pcr_comm_sv_right with (eq:=eq) (mult:=mult). apply eq_Equivalence. intros;ring. intros;ring. apply mult_morph. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)