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. fix psv_comm 1. intros [|dim]. simpl. intros. rewrite <- mult_assoc. rewrite (mult_comm a1). apply mult_assoc. simpl vector. intros a1 a2 [c1 v1]. simpl. split. rewrite <- mult_assoc. rewrite (mult_comm a1). apply mult_assoc. apply psv_comm. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)