∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C},
  Nonempty (CategoryTheory.Limits.LimitBicone F) → CategoryTheory.Limits.HasBiproduct F