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