proposition: Lemma has_finite_limits_has_fiprods : forall a, has_finite_limits a -> has_fiprods a.
proof: Proof. ir. rw has_fiprods_has_limits_over. uh H; ee. ap H0. ap is_finite_vee_cat. uh H; ee; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal