norm_num extension for Nat.sqrt

This module defines a norm_num extension for Nat.sqrt.

theorem Tactic.NormNum.nat_sqrt_helper {x : ℕ} {y : ℕ} {r : ℕ} (hr : y * y + r = x) (hle : Nat.ble r (2 * y) = true) : Nat.sqrt x = y

theorem Tactic.NormNum.isNat_sqrt {x : ℕ} {nx : ℕ} {z : ℕ} : Mathlib.Meta.NormNum.IsNat x nx → Nat.sqrt nx = z → Mathlib.Meta.NormNum.IsNat (Nat.sqrt x) z

def Tactic.NormNum.evalNatSqrt : Mathlib.Meta.NormNum.NormNumExt

Evaluates the Nat.sqrt function.

Equations

• One or more equations did not get rendered due to their size.