In this file are theorems about squares and square roots.
** Module lib_nat_sqrt Imports lib_nat/lib_nat_iter
lib_nat/lib_nat_rels
square = ... : nat->nat
sqrt = ... : nat->nat
sqrt_cor = ... :
{n:nat}and (Le (square (sqrt n)) n) (Lt n (square (suc (sqrt n))))
sqrt_small = ... : {n:nat}(Lt one n)->Lt (sqrt n) n