proposition: Lemma is_uni_oppc : forall c, is_couni c -> is_uni (oppc c).
proof: Proof. ir. cp H. uh H0; ee. uhg. ee. app is_cone_oppc. ir. assert (c = oppc (oppc c)). rww oppc_oppc_cocone. assert (cocone_composable (flip u) c). rw H5. ap cocone_composable_oppc. rw flip_flip. am. assert (cocone_composable (flip v) c). rw H5. ap cocone_composable_oppc. rw flip_flip. am. assert (flip u = flip v). ap H1. am. am. transitivity (oppc (oppc (cocone_compose (flip u) c))). sy. rw oppc_oppc_cocone. reflexivity. app is_cocone_cocone_compose. rw oppc_cocone_compose. rw flip_flip. rw H4. transitivity (oppc (oppc (cocone_compose (flip v) c))). sy. rw oppc_cocone_compose. rw flip_flip. reflexivity. am. rw oppc_oppc_cocone. reflexivity. app is_cocone_cocone_compose. am. transitivity (flip (flip u)). rww flip_flip. rw H8. rww flip_flip. Qed.
imports: Arith limits