proposition: Lemma rcoset_eqP {x y} : reflect (G :* x = G :* y) (x \in G :* y).
proof: Proof. suffices <-: (G :* x == G :* y) = (x \in G :* y) by apply: eqP. by rewrite eqEsubset !mulGS !sub1set rcoset_sym andbb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)