{G : Group} (g h h' : G) (p : g * h = h * g) (p' : g * h' = h' * g) : g * (h * h') = (h * h') * g. Proof. lhs apply simple_associativity. lhs nrapply (ap (.* h') p). lhs_V apply simple_associativity. lhs nrapply (ap (h *.) p'). by apply simple_associativity. 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.