proposition: Lemma sqrt_specif n : (sqrt n)*(sqrt n) <= n < S (sqrt n) * S (sqrt n).
proof: Proof. set (s:=sqrt n). replace n with (n + 0*0 + (0-0)). - apply sqrt_iter_spec; auto. - simpl. now rewrite !add_0_r. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass