∀ (ctx : Int.Linear.Context) (p₁ p₂ : Int.Linear.Poly) (n : ℕ),
  Int.Linear.cooper_right_cert p₁ p₂ n = true →
    Int.Linear.Poly.denote' ctx p₁ ≤ 0 →
      Int.Linear.Poly.denote' ctx p₂ ≤ 0 → Int.Linear.OrOver n (Int.Linear.cooper_right_split ctx p₁ p₂)