Существует ли тактика для решения таких тривиальных задач (бережливое доказательство теорем)?

Я новичок, и я застрял со следующим:

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)

и это кажется настолько тривиальным, что я подумал, что должна быть тактика для ее решения. Но линарит, кольцо, простота, тривиальность не работают.

Итак, я пропустил какой-то важный импорт?

Я также пытался решить это, используя существующие леммы. На первом этапе я хотел достичь:

n : ℕ
⊢ 1 ≠ 2 * n.succ

в надежде, что какая-то тактика более высокого уровня теперь увидит, что это правда. Однако я не знаю, как выполнить какую-либо операцию с обеих сторон уравнения. Разве нельзя как-то разделить обе части на 2?

Мой план состоял в том, чтобы изменить правую сторону на 2*(n+1) и 2n+2 и, возможно, цель

⊢ 0 ≠ 2 * n + 1

в надежде найти применимые леммы в библиотеке.