proposition: Lemma comp_opp : forall a u v, mor (opp a) u -> mor (opp a) v -> source u = target v -> comp (opp a) u v = flip (comp a (flip v) (flip u)).
proof: Proof. ir. assert (axioms a). wr axioms_opp. uh H; ee; am. rw unfold_opp. rw comp_opp'. tv. ap mor_is_mor. wrr unfold_opp. ap mor_is_mor. wrr unfold_opp. tv. am. Qed.
imports: Arith universe