{U : Univalence} (G : Group) (H : Subgroup G) (fin_G : Finite G) (fin_H : Finite H) : nat. Proof. refine (fcard (Quotient (in_cosetL H))). nrapply finite_quotient. 1-5: exact _. intros x y. pose (dec_H := detachable_finite_subset H). apply dec_H. 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.