issubgroup_in_inv' (x : G) : H (- x) -> H x. Proof. intros p; rewrite <- (negate_involutive x); revert p. apply issubgroup_in_inv. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.