proposition: Lemma vsval_unitr w : vsval w \is a GRing.unit -> w \is a GRing.unit.
proof: Proof. case: w => /= u Au Uu; have Au1: u^-1 \in A by rewrite memvV. apply/unitrP; exists (Subvs Au1). by split; apply: val_inj; rewrite /= ?mulrV ?mulVr ?(unitr_algid1 Au). 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)