proposition: Lemma abmonoidoprer {X : UU} {opp : binop X} (is : isabmonoidop opp) (a b c d : X) : paths (opp (opp a b) (opp c d)) (opp (opp a c) (opp b d)).
proof: Proof. destruct is as [ is comm ]. destruct is as [ assoc unital0 ]. simpl in *. destruct (assoc (opp a b) c d). destruct (assoc (opp a c) b d). destruct (pathsinv0 (assoc a b c)). destruct (pathsinv0 (assoc a c b)). destruct (comm b c). apply idpath. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions