proposition: Lemma lemma1 : f (- mon_unit) = a * c.
proof: Proof. unfold f; apply ap. exact (hspace_right_identity c). Defined.
imports: Classes.interfaces.abstract_algebra Cubical Pointed.Core Pointed.pSusp Homotopy.HSpace.Core Homotopy.Suspension Homotopy.Join.Core