proposition: Lemma is_cocone_oppc : forall c, is_cone c -> is_cocone (oppc c).
proof: Proof. ir. cp H; uh H; uhg; ee. uh H; uhg. rw vertex_oppc. rw coedge_nt_oppc. uf oppc. tv. rw coedge_nt_oppc. app oppnt_axioms. rw cocone_target_oppc. rw ob_opp. rw vertex_oppc. am. am. rw coedge_nt_oppc. rw target_oppnt. rw source_edge_nt. rw cocone_source_oppc. rw cocone_target_oppc. rw vertex_oppc. rw oppf_constant_functor. reflexivity. app cone_source_axioms. app Limit.ob_vertex. am. am. am. am. Qed.
imports: Arith limits