{U : Univalence} (G : Group) (H : Subgroup G) (fin_G : Finite G) (fin_H : Finite H) : exists d, d * (fcard H) = fcard G. Proof. exists (subgroup_index G H _ _). symmetry. refine (fcard_quotient (in_cosetL H) @ _). refine (_ @ finadd_const _ _). apply ap, path_forall. srapply Quotient_ind_hprop. simpl. intros x. apply fcard_equiv'. simpl. snrapply equiv_functor_sigma. 2: apply (isequiv_group_left_op (-x)). 1: hnf; trivial. exact _. 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.