proposition: Lemma mk_invgK : involutive invg.
proof: Proof. have mulV21 x: x^-1^-1 * 1 = x by rewrite -(mulVg x) mulgA mulVg mul1g. by move=> x; rewrite -[_ ^-1]mulV21 -(mul1g 1) mulgA !mulV21. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)