proposition: Lemma edge_oppc : forall c x, ob (cocone_source c) x -> is_cocone c -> edge (oppc c) x = flip (coedge c x).
proof: Proof. ir. uf edge. rw edge_nt_oppc. rw ntrans_oppnt. tv. app coedge_nt_axioms. rw osource_coedge_nt. am. Qed.
imports: Arith limits