proposition: Lemma has_finite_limits_has_cofiprods : forall a, has_finite_colimits a -> has_cofiprods a.
proof: Proof. ir. rw has_cofiprods_has_colimits_over_opp. uh H; ee. ap H0. ap is_finite_cat_opp. ap is_finite_vee_cat. uh H; ee; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal