Unit action preserves nonnegativity
Provedpell_action_nonnegnumber-theorypell-equation
Composing nonnegative solutions with nonnegative units stays nonnegative (for ). Keeps descended Pell solutions in the positive quadrant.
Preamble
import Mathlib.Tactic
Formal statement
theorem pell_action_nonneg {D x y u v : Int} (hD : 0 ≤ D) (hx : 0 ≤ x) (hy : 0 ≤ y) (hu : 0 ≤ u) (hv : 0 ≤ v) : 0 ≤ u * x + D * v * y ∧ 0 ≤ v * x + u * y := by sorrySource