proposition: Lemma composable_opp : forall a u v, axioms a -> composable (opp a) u v = composable a (flip v) (flip u).
proof: Proof. ir. ap iff_eq; ir. rwi composable_facts_rw H0; ap show_composable; try (wr mor_opp; lu); try (rw mor_opp; lu). rw source_flip. rw target_flip; try (sy; lu). apply mor_arrow_like with (opp a); lu. apply mor_arrow_like with (opp a); lu. rwi composable_facts_rw H0. ap show_composable. uh H0; ee. rww mor_opp. rww mor_opp. lu. uh H0; ee. wr source_flip. wr target_flip. sy; am. rw like_flip. apply mor_arrow_like with a; lu. rw like_flip; apply mor_arrow_like with a; lu. Qed.
imports: Arith universe