nlinarith
nlinarith
は 非線形(non-linear)な式も扱えるように linarith
にいくつか前処理を追加したものです。
import Mathlib.Tactic.Linarith -- `linarith` や `nlinarith` を使うため
variable (a b : ℕ)
example (h : a ≤ b) : a ^ 2 ≤ b ^ 2 := by
-- `linarith` では示すことができない
fail_if_success linarith
nlinarith