Lemma abmonoidoprer {X : UU} {opp : binop X} (is : isabmonoidop opp) (a b c d : X) : opp (opp a b) (opp c d) = opp (opp a c) (opp b d). Proof. induction is as [ is comm ]. induction is as [ assoc unital0 ]. simpl in *. induction (assoc (opp a b) c d). induction (assoc (opp a c) b d). induction (!assoc a b c). induction (!assoc a c b). induction (comm b c). apply idpath. Defined.