proposition: Lemma mor_opp' : forall a u, axioms a -> mor (opp' a) u = mor a (flip u).
proof: Proof. ir. assert (lem : forall b v, axioms b -> mor (opp' b) v -> mor b (flip v)). ir. uhg; ee. am. uh H1; ee. rwi is_mor_opp' H2. am. ap iff_eq; ir. au. assert (u = flip (flip u)). rw flip_flip; tv. uhg; ee. ap opp'_axioms. am. rw is_mor_opp'. app mor_is_mor. Qed.
imports: Arith universe