{A B : Group} (f : GroupHomomorphism A B) (x y : A) : f (x * -y) = group_unit <~> (f x = f y). Proof. refine (grp_moveL_1M oE equiv_concat_l _^ _). lhs nrapply grp_homo_op. apply ap, grp_homo_inv. Defined.
Require Import Basics Types HProp HFiber HSet. Require Import Homotopy.IdentitySystems. Require Import (notations) Classes.interfaces.canonical_names. Require Import Pointed.Core. Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Int. Require Import Truncations.Core.