proposition: Lemma sum_index_rcosets_cycle : (\sum_(x in X) n_ x)%N = #|G : H|.
proof: Proof. by rewrite [#|G : H|](card_partition partHGg) -defHgX big_imset. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype bigop ssralg finset fingroup) mathcomp(morphism perm finalg action gproduct commutator) mathcomp(cyclic)