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