proposition: Lemma LagrangeI G H : (#|G :&: H| * #|G : H|)%N = #|G|.
proof: Proof. rewrite -[#|G|]sum1_card (partition_big_imset (rcoset H)) /=. rewrite mulnC -sum_nat_const; apply: eq_bigr => _ /rcosetsP[x Gx ->]. rewrite -(card_rcoset _ x) -sum1_card; apply: eq_bigl => y. by rewrite rcosetE (sameP eqP rcoset_eqP) group_modr ?sub1set // !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)