proposition: Lemma sqrt_spec p : let s := sqrt p in s*s <= p < (succ s)*(succ s).
proof: Proof. simpl. assert (H:=sqrtrem_spec p). unfold sqrt in *. destruct sqrtrem as (s,rm); simpl. inversion_clear H; subst. - split. + reflexivity. + apply mul_lt_mono; apply lt_succ_diag_r. - split. + apply lt_le_incl, lt_add_r. + rewrite <- add_1_l, mul_add_distr_r, !mul_add_distr_l, !mul_1_r, !mul_1_l. rewrite add_assoc, (add_comm _ _). apply add_lt_mono_r. now rewrite <- add_assoc, add_diag, add_1_l, lt_succ_r. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef