{U : Univalence} (G : Group) (H : NormalSubgroup G) (fin_G : Finite G) (fin_H : Finite H) : fcard (QuotientGroup G H) * fcard H = fcard G. Proof. apply lagrange. Defined.
Require Import Basics Types. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.Subgroup. Require Import Algebra.Groups.QuotientGroup. Require Import Spaces.Finite.Finite. Require Import Spaces.Nat.Core.