proposition: Lemma mulVr : {in unit, left_inverse 1 inv *%R}.
proof: Proof. rewrite /inv => x Ux; case: pickP => [y | no_y]; last by case/pred0P: Ux. by case/andP=> _; move/eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype finset fingroup morphism perm action) mathcomp(ssralg countalg)