mathlib documentation

data.nat.sqrt_norm_num

norm_num plugin for sqrt #

The norm_num plugin evaluates sqrt by bounding it between consecutive integers.

theorem norm_num.is_sqrt {n a a2 b : } (ha2 : a * a = a2) (hb : a2 + b = n) (hle : b bit0 a) :

Given n provides (a, ⊢ nat.sqrt n = a).

meta def norm_num.eval_sqrt  :

A norm_num plugin for sqrt n when n is a numeral.