proposition: Theorem Lagrange G H : H \subset G -> (#|H| * #|G : H|)%N = #|G|.
proof: Proof. by move/setIidPr=> sHG; rewrite -{1}sHG LagrangeI. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)