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