Documentation

Mathlib.Tactic.NormNum.NatSqrt

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) :