proposition: Lemma sqrt_iter_spec : forall k p q r, q = p+p -> r<=q -> let s := sqrt_iter k p q r in s*s <= k + p*p + (q - r) < (S s)*(S s).
proof: Proof. intro k; induction k as [|k IHk]. - simpl; intros p q r Hq Hr. split. + apply le_add_r. + apply lt_succ_r. rewrite mul_succ_r, add_assoc, (add_comm p), <- add_assoc. apply add_le_mono_l. rewrite <- Hq. apply le_sub_l. - intros p q r; destruct r as [|r]. + intros Hq _. replace (S k + p*p + (q-0)) with (k + (S p)*(S p) + (S (S q) - S (S q))). 2:{ rewrite sub_diag, sub_0_r, add_0_r. simpl. rewrite add_succ_r; f_equal. rewrite <- add_assoc; f_equal. rewrite mul_succ_r, (add_comm p), <- add_assoc. now f_equal. } apply IHk; simpl. * now rewrite add_succ_r, Hq. * apply le_n. + intros Hq Hr. replace (S k + p*p + (q-S r)) with (k + p*p + (q - r)) by (simpl; rewrite <- add_succ_r; f_equal; rewrite <- sub_succ_l; trivial). apply IHk; trivial. apply le_trans with (S r); trivial. do 2 constructor. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass