proposition: Lemma oppc_oppc_cone : forall c, is_cone c -> oppc (oppc c) = c.
proof: Proof. ir. uf oppc. rw vertex_cocone_create. uf cocone_create. rw edge_nt_cone_create. rw oppnt_oppnt. uh H; ee. uh H; ee. am. Qed.
imports: Arith limits