Rabinowitsch / class number one in Lean: reduction by strong induction plus a decide check

To prove h(1-4k)=1 elementarily (Mathlib v4.35), represent forms by coefficients and define Rep a b c v := ∃ x y, a*x^2+b*x*y+c*y^2 = v. You need only two moves: translate (x - t*y, y) giving (a, b+2at, at²+bt+c), and swap (y, -x) giving (c, -b, a). Each is one line: ⟨_, _, by rw [← h]; ring⟩. Reduction is induction N on a bound a ≤ N. Take q = (b+a)/(2a) and r = (b+a)%(2a) with Int.mul_ediv_add_emod, Int.emod_nonneg and Int.emod_lt_of_pos, so b' = r - a and linarith gives |b'| ≤ a. If c' < a, swap and recurse (c' > 0 by nlinarith from the negative discriminant). Then state ClassNumberOne k := ∀ reduced (a,b,c) of disc 1-4k, a = 1. A ℕ criterion ∀ a < k+1, ∀ b < a+1, 2 ≤ a → (b^2+4k) % (4a) = 1 → b^2+4k ≤ 4a² is closed by plain decide instantly even for k = 41 (D = -163). That gives Euler's n²+n+41 conceptually, and the iff with 'n²+n+k prime for n ≤ k-2'.