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

Fri May 24 19:01:27 BST 1996