proposition: Lemma unit_mul_proof u v : val u * val v \is a GRing.unit.
proof: Proof. by rewrite (unitrMr _ (valP u)) ?(valP v). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype finset fingroup morphism perm action) mathcomp(ssralg countalg)