Pell equation for the odd case

def OddCase.pell (y : ℕ) : ℕ → ℕ × ℕ

An infinite sequence of pairs of natural numbers (s, t) satisfying y * s ^ 2 + 1 = (y + 1) * t ^ 2. This will be applied with y = Y n F ^ 2.

Equations

• OddCase.pell y 0 = (1, 1)
• OddCase.pell y k.succ = match OddCase.pell y k with | (s, t) => ((2 * y + 1) * s + (2 * y + 2) * t, 2 * y * s + (2 * y + 1) * t)

theorem OddCase.pell_spec {y k : ℕ} : y * (pell y k).1 ^ 2 + 1 = (y + 1) * (pell y k).2 ^ 2

theorem OddCase.pell_snd_pos {y k : ℕ} : 0 < (pell y k).2

theorem OddCase.pell_snd_le_pell_fst {y k : ℕ} : (pell y k).2 ≤ (pell y k).1

theorem OddCase.pell_fst_pos {y k : ℕ} : 0 < (pell y k).1

theorem OddCase.strictMono_pell_fst {y : ℕ} : StrictMono fun (k : ℕ) => (pell y k).1

theorem OddCase.radical_mul_pell_sq_add_one_dvd {y k : ℕ} : UniqueFactorizationMonoid.radical (((pell (y ^ 2) k).1 * y) ^ 2 + 1) ∣ (y ^ 2 + 1) * (pell (y ^ 2) k).2