English
The y-sequence satisfies the successor formula yz(a1,n+1) = xz(a1,n) + yz(a1,n)·az(a).
Русский
Последовательность y удовлетворяет формуле перехода yz(a1,n+1) = xz(a1,n) + yz(a1,n)·az(a).
LaTeX
$$$ yz(a1, n+1) = xz(a1, n) + yz(a1, n) \cdot az(a) $$$
Lean4
instance dnsq : Zsqrtd.Nonsquare (d a1) :=
⟨fun n h =>
have : n * n + 1 = a * a := by rw [← h]; exact Nat.succ_pred_eq_of_pos (asq_pos a1)
have na : n < a := Nat.mul_self_lt_mul_self_iff.1 (by rw [← this]; exact Nat.lt_succ_self _)
have : (n + 1) * (n + 1) ≤ n * n + 1 := by rw [this]; exact Nat.mul_self_le_mul_self na
have : n + n ≤ 0 := @Nat.le_of_add_le_add_right _ (n * n + 1) _ (by ring_nf at this ⊢; assumption)
Nat.ne_of_gt (d_pos a1) <| by rwa [Nat.eq_zero_of_le_zero ((Nat.le_add_left _ _).trans this)] at h⟩
