proposition: Lemma coedge_oppc : forall c x, ob (cone_source c) x -> is_cone c -> coedge (oppc c) x = flip (edge c x).
proof: Proof. ir. uf coedge. rw coedge_nt_oppc. rw ntrans_oppnt. tv. app edge_nt_axioms. rw osource_edge_nt. am. am. Qed.
imports: Arith limits