proposition: Lemma pmc_comm_sv_right : forall dim (m:matrix dim) (c : vector dim) (a:A), prod_mat_col _ m (prod_scal_vec _ a c) ==v prod_scal_vec _ a (prod_mat_col _ m c).
proof: Proof. fix pmc_comm_sv_right 1. intros [|dim]. simpl. intros;rewrite <- mult_assoc. rewrite (mult_comm m);apply mult_assoc. simpl vector;simpl matrix. intros [a1 [r1 [c1 m1]]] [a2 r2] a. simpl. repeat rewrite mult_distrib_right. constructor. rewrite <- (mult_assoc a1). rewrite (mult_comm a1); rewrite mult_assoc. rewrite prc_comm_sv_right. reflexivity. repeat rewrite psv_distrib_right. rewrite <- psv_assoc. rewrite pmc_comm_sv_right. reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)