{G : Group} (g h k : G) (p : centralizer g h) (q : centralizer g k) : centralizer g (h * k). Proof. refine (grp_assoc _ _ _ @ _). refine (ap (fun x => x * k) p @ _). refine ((grp_assoc _ _ _)^ @ _). refine (ap (fun x => h * x) q @ _). apply grp_assoc. Defined.
Require Import Basics Types Truncations.Core. Require Import HFiber AbelianGroup.