proposition: Lemma psv_assoc : forall dim c1 c2 (r:vector dim), prod_scal_vec _ c1 (prod_scal_vec _ c2 r) ==v prod_scal_vec _ (mult c1 c2) r .
proof: Proof. fix psv_assoc 1. intros [|dim]. simpl. intros. symmetry; apply mult_assoc. simpl vector. intros c1 c2 [a r]. simpl. split. symmetry; apply mult_assoc. apply psv_assoc. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)