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 : r.ble (2 * y) = true) : x.sqrt = y

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

def Tactic.NormNum.proveNatSqrt (ex : Q(ℕ)) : (ey : Q(ℕ)) × Q(«$ex».sqrt = «$ey»)

Given the natural number literal ex, returns its square root as a natural number literal and an equality proof. Panics if ex isn't a natural number literal.

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

Evaluates the Nat.sqrt function.