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