proposition: Lemma is_coversal_oppc : forall c, is_versal c -> is_coversal (oppc c).
proof: Proof. ir. uh H; uhg; ee. app is_cocone_oppc. ir. cp H2. rwi cosocle_oppc H3. util (H0 (oppc b)). app is_cone_oppc. rw socle_oppc. rw H3. rw oppf_oppf. tv. am. nin H4. ee. assert (cocone_composable (flip x) (oppc c)). app cocone_composable_oppc. rww flip_flip. sh (flip x). ee; try am. transitivity (oppc (oppc b)). wr H5. sy. rw oppc_cone_compose. reflexivity. am. rww oppc_oppc_cocone. am. Qed.
imports: Arith limits