proposition: Lemma class_supportGidl A x : x \in G -> class_support (A :^ x) G = class_support A G.
proof: Proof. by move=> Gx; rewrite -class_support_set1r -class_supportM lcoset_id. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)