∀ (ctx : Int.Linear.Context) (p₁ p₂ : Int.Linear.Poly) (k : ℕ),
  Int.Linear.cooper_right_split ctx p₁ p₂ k =
    (Int.Linear.Poly.denote' ctx
          (((p₁.tail.mul_k p₂.leadCoeff).combine (p₂.tail.mul_k (-p₁.leadCoeff))).addConst (-p₁.leadCoeff * ↑k)) ≤
        0 ∧
      p₂.leadCoeff ∣ Int.Linear.Poly.denote' ctx (p₂.tail.addConst ↑k))