Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype. Require Import div path bigop prime finset fingroup. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Section LaGrange. Variable gT : finGroupType. Implicit Types G H : {group gT}. Open Scope group_scope. Lemma TutorialLaGrange G H : H \subset G -> (#|H| * #|G : H|)%N = #|G|. move/setIidPr. move=> {1}<-. rewrite mulnC. rewrite -sum_nat_const. rewrite -[#|G|]sum1_card. rewrite (partition_big_imset (rcoset H)) /= -/(rcosets H G) /=. apply: eq_bigr => /= Hg. case/rcosetsP. move=> g Gg -> {Hg}. rewrite -(card_rcoset _ g). rewrite -sum1_card. apply: eq_bigl => k. rewrite group_modr ?sub1set //. rewrite inE. congr (_ && _). rewrite rcosetE. apply/idP/eqP. by apply: rcoset_transl. move=> <-. rewrite -[X in X \in _](mul1g k). rewrite mem_mulg //. by rewrite in_set1. Qed.