proposition: Lemma is_cone_oppc : forall c, is_cocone c -> is_cone (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 cone_target_oppc. rw ob_opp. rw vertex_oppc. am. am. rw edge_nt_oppc. rw source_oppnt. rw target_coedge_nt. rw cone_source_oppc. rw cone_target_oppc. rw vertex_oppc. rw oppf_constant_functor. reflexivity. app cocone_source_axioms. app ob_vertex. am. am. am. am. Qed.
imports: Arith limits