proposition: Lemma actsRs_rcosets H G : [acts G, on rcosets H G | 'Rs].
proof: Proof. by rewrite -orbitRs acts_orbit ?subsetT. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)