proposition: Lemma is_colimit_of_oppf : forall f a, is_limit_of f a -> is_colimit_of (oppf f) (oppc a).
proof: Proof. ir. uhg; ee. ap is_colimit_oppc. uh H; ee; am. rw cosocle_oppc. uh H; ee. rww H0. uh H; ee. uh H; ee. uh H; ee. am. Qed.
imports: Arith limits