proposition: Lemma prodvA : associative prodv.
proof: Proof. move=> U V W; rewrite -(span_basis (vbasisP U)) span_def !big_distrl /=. apply: eq_bigr => u _; rewrite -(span_basis (vbasisP W)) span_def !big_distrr. apply: eq_bigr => w _; rewrite -(span_basis (vbasisP V)) span_def /=. rewrite !(big_distrl, big_distrr) /=; apply: eq_bigr => v _. by rewrite !prodv_line mulrA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop ssralg) mathcomp(finalg zmodp matrix vector poly)