proposition: Lemma comp_opp' : forall a u v, is_mor (opp' a) u -> is_mor (opp' a) v -> source u = target v -> comp (opp' a) u v = flip (comp a (flip v) (flip u)).
proof: Proof. ir. uf opp'. rw comp_create. tv. rww inc_image_create_flip. rww inc_image_create_flip. am. Qed.
imports: Arith universe