Square Roots

In this file are theorems about squares and square roots.

 ** Module lib_nat_sqrt Imports lib_nat_iter lib_nat_rels
  square = ... : nat->nat
  sqrt = ... : nat->nat
  sqrt_cor = ... :
    {n:nat}(Le (square (sqrt n)) n /\ Lt n (square (suc (sqrt n))))
  sqrt_small = ... : {n:nat}(Lt one n)->Lt (sqrt n) n