proposition: Lemma is_mor_opp' : forall a u, is_mor (opp' a) u = is_mor a (flip u).
proof: Proof. ir. uf opp'. rw is_mor_create. rw Image.inc_rw. app iff_eq; ir. nin H. ee. wr H0. rw flip_flip. am. sh (flip u). ee. am. rww flip_flip. Qed.
imports: Arith universe