{G : Group} (g h : G) (p : centralizer g h) : centralizer g (-h). Proof. unfold centralizer in *. symmetry. refine ((grp_unit_r _)^ @ _ @ grp_unit_l _). refine (ap (fun x => (-h * g * x)) (grp_inv_r h)^ @ _ @ ap (fun x => x * (g * -h)) (grp_inv_l h)). refine (grp_assoc _ _ _ @ _ @ (grp_assoc _ _ _)^). refine (ap (fun x => x * (-h)) _). refine ((grp_assoc _ _ _)^ @ _ @ grp_assoc _ _ _). exact (ap (fun x => (-h) * x) p). Defined.
Require Import Basics Types Truncations.Core. Require Import HFiber AbelianGroup.