proposition: Lemma mor_opp : forall a u, mor (opp a) u = mor a (flip u).
proof: Proof. ir. ap iff_eq; ir. assert (axioms a). wr axioms_opp. uh H; ee; am. rwi unfold_opp H. rwi mor_opp' H. am. am. am. assert (axioms a). uh H; ee; am. rww unfold_opp. rww mor_opp'. Qed.
imports: Arith universe