proposition: Lemma iter_sqrt_correct n rec i j: 0 < φ i -> 0 < φ j -> φ i < (φ j + 1) ^ 2 -> 2 * φ j < wB -> (forall j1, 0 < φ j1 -> 2^(Z_of_nat n) + φ j1 <= φ j -> φ i < (φ j1 + 1) ^ 2 -> 2 * φ j1 < wB -> φ (rec i j1) ^ 2 <= φ i < (φ (rec i j1) + 1) ^ 2) -> φ (iter_sqrt n rec i j) ^ 2 <= φ i < (φ (iter_sqrt n rec i j) + 1) ^ 2.
proof: Proof. revert rec i j; elim n; unfold iter_sqrt; fold iter_sqrt; clear n. - intros rec i j Hi Hj Hij H31 Hrec; apply sqrt_step_correct. 1-4: lia. intros; apply Hrec; only 2: rewrite Zpower_0_r; auto with zarith. - intros n Hrec rec i j Hi Hj Hij H31 HHrec. apply sqrt_step_correct; auto. intros j1 Hj1 Hjp1; apply Hrec; auto with zarith. intros j2 Hj2 H2j2 Hjp2 Hj31; apply Hrec; auto with zarith. intros j3 Hj3 Hpj3. apply HHrec; auto. rewrite -> inj_S, Z.pow_succ_r. + apply Z.le_trans with (2 ^Z_of_nat n + φ j2); auto with zarith. + apply Zle_0_nat. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63