proposition: Lemma invr_out : {in [predC unit], inv =1 id}.
proof: Proof. rewrite /inv => x nUx; case: pickP => // y invxy. by case/existsP: nUx; exists y. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype finset fingroup morphism perm action) mathcomp(ssralg countalg)