proposition: Lemma groupMl x y : x \in G -> (x * y \in G) = (y \in G).
proof: Proof. move=> Gx; apply/idP/idP=> [Gxy|]; last exact: groupM. by rewrite -(mulKg x y) groupM ?groupVr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)