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