proposition: Lemma is_couni_oppc : forall c, is_uni c -> is_couni (oppc c).
proof: Proof. ir. cp H. uh H0; ee. uhg. ee. app is_cocone_oppc. ir. assert (c = oppc (oppc c)). rww oppc_oppc_cone. assert (cone_composable c (flip u)). rw H5. ap cone_composable_oppc. rw flip_flip. am. assert (cone_composable c (flip v)). rw H5. ap cone_composable_oppc. rw flip_flip. am. assert (flip u = flip v). ap H1. am. am. transitivity (oppc (oppc (cone_compose c (flip u)))). sy. rw oppc_oppc_cone. reflexivity. rww is_cone_cone_compose. rw oppc_cone_compose. rw flip_flip. rw H4. transitivity (oppc (oppc (cone_compose c (flip v)))). sy. rw oppc_cone_compose. rw flip_flip. reflexivity. am. rw oppc_oppc_cone. reflexivity. rww is_cone_cone_compose. am. transitivity (flip (flip u)). rww flip_flip. rw H8. rww flip_flip. Qed.
imports: Arith limits