proposition: Lemma unit_inv_proof u : (val u)^-1 \is a GRing.unit.
proof: Proof. by rewrite unitrV ?(valP u). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype finset fingroup morphism perm action) mathcomp(ssralg countalg)