Lean4中自然数命题q + q² ≠7的简化证明问询

问题1：简化模式匹配证明的实现 #

你给出的雏形代码可以直接用数字字面量（0/1/2）做模式匹配，不需要强制使用zero和succ q，Lean 4支持对自然数直接匹配具体数值。补充完整后的代码如下：

example (q : Nat) : q + q ^ 2 ≠ 7 := by
  match q with
  | 0 => norm_num
  | 1 => norm_num
  | 2 => norm_num
  | n+3 => -- 匹配所有≥3的自然数，等价于n≥0时n+3≥3
    have h : 9 ≤ (n+3) * (n+3) := by exact Nat.mul_le_mul (by norm_num) (by norm_num)
    rw [← Nat.pow_two] at h
    linarith only [h]

用n+3匹配≥3的自然数比_更直观，能明确范围，后续的不等式证明逻辑和你原代码一致，linarith会自动结合目标矛盾完成证明。

问题2：更简洁的证明思路 #

思路1：区间拆分一键验证

利用interval_cases战术自动拆分自然数为有限具体值和无限区间，再用norm_num直接验证所有情况：

example (q : Nat) : q + q ^ 2 ≠ 7 := by
  interval_cases q <;> norm_num

interval_cases会自动把q拆分为0、1、2三个具体值，以及≥3的区间，norm_num能直接计算具体值的结果，同时验证≥3时q+q²≥12>7的矛盾。

思路2：质数性质反证

将原式整理为q(q+1)=7，利用7是质数的性质导出矛盾：连续自然数q和q+1互质，不可能同为质数7的因数：

example (q : Nat) : q + q ^ 2 ≠ 7 := by
  intro h
  have : q * (q + 1) = 7 := by rw [← h, Nat.add_mul_self_eq_mul_succ]
  have prime7 : Nat.Prime 7 := by norm_num
  rw [Nat.Prime.eq_one_or_self_of_dvd prime7] at this
  cases this with
  | inl h1 => rw [h1] at this; norm_num at this
  | inr h2 => rw [h2] at this; norm_num at this

内容的提问来源于stack exchange，提问作者DBE