proposition: Lemma class_supportD1 A : (class_support A G)^# = cover (A^# :^: G).
proof: Proof. rewrite cover_imset class_supportEr setDE big_distrl /=. by apply: eq_bigr => x _; rewrite -setDE conjD1g. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)