fact: Definition bloop_inv {G : Group} : forall x : G, bloop (-x) = (bloop x)^.
imports: Basics Types Pointed Cubical WildCat Algebra.AbGroups Homotopy.HSpace.Core TruncType Truncations.Core Truncations.Connectedness Homotopy.HomotopyGroup Homotopy.WhiteheadsPrinciple