∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I₁ : R →+* R}
  [inst_3 : Preorder R] [AddLeftMono R] {B C : M →ₛₗ[I₁] M →ₗ[R] R},
  B.IsPosSemidef → C.IsPosSemidef → (B + C).IsPosSemidef