{G : Group} {X} {g : G} : subgroup_generated_type X g -> subgroup_generated_type X (- g). Proof. intros p. rewrite <- left_identity. exact (sgt_op sgt_unit p). Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.