proposition: Lemma pcr_comm_sv_left : forall dim (c r : vector dim) (a:A), prod_col_row _ (prod_scal_vec _ a r) c ==m prod_scal_mat _ a (prod_col_row _ r c).
proof: Proof. fix pcr_comm_sv_left 1. intros [|dim]. simpl. intros;rewrite <- mult_assoc. reflexivity. simpl vector. intros [a1 r1] [a2 c2] a. simpl. refine (conj _ (conj _ (conj _ _ ))). apply mult_assoc. symmetry; apply psv_assoc. rewrite psv_assoc. rewrite mult_comm. symmetry;apply psv_assoc. apply pcr_comm_sv_left. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)