proposition: Lemma psv_comm : forall dim (a1 a2:A) (v:vector dim), prod_scal_vec _ a1 (prod_scal_vec _ a2 v) ==v prod_scal_vec _ a2 (prod_scal_vec _ a1 v).
proof: Proof. apply (psv_comm eq_Equivalence) with (mult:=mult);try (intros;ring). apply mult_morph. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)