Unconditional nonnegativity of the pressure constants.

theorem CKN.pressureP234Constant_nonneg' : 0 ≤ pressureP234Constant

The unconditional nonnegativity of pressureP234Constant.

theorem CKN.pressureP56Constant_nonneg' : 0 ≤ pressureP56Constant

The unconditional nonnegativity of pressureP56Constant.

theorem CKN.pressureP13Constant_nonneg' (q : ℝ) : 0 ≤ pressureP13Constant q

The unconditional nonnegativity of pressureP13Constant q for any real q.

theorem CKN.pressureP12Constant_nonneg : 0 ≤ pressureP12Constant

The unconditional nonnegativity of pressureP12Constant.