f (conj c * conj a * d * conj b) = (-d) * conj b. Proof. unfold f. rewrite 2 factorneg_r. rewrite 3 simple_associativity. rewrite <- distropp. rewrite (right_inverse (a * c)). rewrite (left_identity d). symmetry. apply factorneg_l. Defined.
Require Import Classes.interfaces.abstract_algebra. Require Import Cubical.DPath Cubical.PathSquare. Require Import Pointed.Core Pointed.pSusp. Require Import Homotopy.HSpace.Core. Require Import Homotopy.Suspension. Require Import Homotopy.Join.Core.