proposition: Lemma prodv_id A : (A * A)%VS = A.
proof: Proof. apply/eqP; rewrite eqEsubv asubv; apply/subvP=> u Au. by rewrite -(algidl Au) memv_mul // memv_algid. 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)