proposition: Lemma Lagrange_index G H K : H \subset G -> K \subset H -> (#|G : H| * #|H : K|)%N = #|G : K|.
proof: Proof. move=> sHG sKH; apply/eqP; rewrite mulnC -(eqn_pmul2l (cardG_gt0 K)). by rewrite mulnA !Lagrange // (subset_trans sKH). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)