** 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