proposition: Lemma sqrt_spec : forall x, φ (sqrt x) ^ 2 <= φ x < (φ (sqrt x) + 1) ^ 2.
proof: Proof. intros i; unfold sqrt. rewrite compare_spec. case Z.compare_spec; rewrite to_Z_1; intros Hi. - lia. - apply iter_sqrt_correct; auto with zarith; rewrite lsr_spec, to_Z_1; change (2^1) with 2; auto with zarith. + replace φ i with (1 * 2 + (φ i - 2))%Z; try ring. assert (0 <= (φ i - 2)/2)%Z by (apply Z_div_pos; auto with zarith). rewrite Z_div_plus_full_l; auto with zarith. + apply sqrt_init; auto. + assert (W:= Z_mult_div_ge φ i 2);assert (W':= to_Z_bounded i);auto with zarith. + intros j2 H1 H2; contradict H2; apply Zlt_not_le. fold wB;assert (W:=to_Z_bounded i). apply Z.le_lt_trans with (φ i); auto with zarith. assert (0 <= φ i/2)%Z by (apply Z_div_pos; auto with zarith). apply Z.le_trans with (2 * (φ i/2)); auto with zarith. apply Z_mult_div_ge; auto with zarith. - case (to_Z_bounded i); repeat rewrite Z.pow_2_r; auto with zarith. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63