有没有解决这些琐碎目标的策略(精益定理证明)

Question

我是一个初学者，我被以下内容所困扰：

import tactic.linarith
import tactic.suggest
noncomputable theory
open_locale classical
lemma two_ne_four_mul_any (n:ℕ) : 2 ≠ 2 * 2 * n := begin
cases n,
linarith,
rw mul_assoc,
???
end

现在的状态是：

n : ℕ
⊢ 2 ≠ 2 * (2 * n.succ)

它太琐碎了，我想一定有解决它的策略。但linarith、ring、simp、琐碎都不起作用。

那么，我错过了一些重要的进口吗？

我还试图使用现有的引理来解决这个问题。在我想达到的第一步：

n : ℕ
⊢ 1 ≠ 2 * n.succ

希望一些更高级别的策略现在能看到这是真的。然而，我不知道如何对等式的两边进行运算。难道不应该以某种方式把双方都除以2吗？

我的计划是将rhs改为2*(n+1(和2n+2，也许目标是

⊢ 0 ≠ 2 * n + 1

希望在图书馆中找到适用的引理。

Answer 1

linarith知道线性算术，这是一个线性算术目标，但由于nat.succ的使用而变得模糊。如果你把它重写掉，那么linarith就会起作用。

example (n : ℕ): 2 ≠ 2 * (2 * n.succ) :=
by rw nat.succ_eq_add_one; linarith