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