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. fix pcr_comm_sv_right 1. intros [|dim]. simpl. intros;rewrite <- mult_assoc. rewrite (mult_comm c). apply mult_assoc. simpl vector. intros [a1 r1] [a2 c2] a. simpl. rewrite pcr_comm_sv_right. rewrite <- mult_assoc. rewrite (mult_comm a1). rewrite mult_assoc. refine (conj _ (conj _ (conj _ _))). reflexivity. apply psv_comm. symmetry. apply psv_assoc. reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)