proposition: Lemma invmK : {in f @* G, cancel invm f}.
proof: Proof. by move=> fx; case/morphimP=> x _ Gx ->; rewrite invmE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)