H (x * y) -> H x -> H y := issubgroup_in_op_r x y. End SubgroupElements. Global Instance isequiv_subgroup_in_inv `(H : Subgroup G) (x : G) : IsEquiv (subgroup_in_inv H x). Proof. srapply isequiv_iff_hprop. apply subgroup_in_inv'. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.