proposition: Lemma cardJg A x : #|A :^ x| = #|A|.
proof: Proof. by rewrite (card_imset _ (conjg_inj x)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)