proposition: Lemma iter2_sqrt_correct n rec ih il j: 2^(Z_of_nat (size - 2)) <= φ ih -> 0 < φ j -> Φ (WW ih il) < (φ j + 1) ^ 2 -> (forall j1, 0 < φ j1 -> 2^(Z_of_nat n) + φ j1 <= φ j -> Φ (WW ih il) < (φ j1 + 1) ^ 2 -> φ (rec ih il j1) ^ 2 <= Φ (WW ih il) < (φ (rec ih il j1) + 1) ^ 2) -> φ (iter2_sqrt n rec ih il j) ^ 2 <= Φ (WW ih il) < (φ (iter2_sqrt n rec ih il j) + 1) ^ 2.
proof: Proof. revert rec ih il j; elim n; unfold iter2_sqrt; fold iter2_sqrt; clear n. - intros rec ih il j Hi Hj Hij Hrec; apply sqrt2_step_correct. 1-3: lia. intros; apply Hrec; only 2: rewrite Zpower_0_r; auto with zarith. - intros n Hrec rec ih il j Hi Hj Hij HHrec. apply sqrt2_step_correct; auto. intros j1 Hj1 Hjp1; apply Hrec; auto with zarith. intros j2 Hj2 H2j2 Hjp2; 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)%Z; auto with zarith. + apply Zle_0_nat. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63