proposition: Lemma invg_set1 x : [set x]^-1 = [set x^-1].
proof: Proof. by apply/setP=> y; rewrite !inE inv_eq //; apply: invgK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)