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