proposition: Fact regular_vect_iso : Vector.axiom 1 R^o.
proof: Proof. exists (fun a => a%:M) => [a b c|]; first by rewrite rmorphD scale_scalar_mx. by exists (fun A : 'M_1 => A 0 0) => [a | A]; rewrite ?mxE // -mx11_scalar. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)