proposition: Lemma sqrt_step_correct rec i j: 0 < φ i -> 0 < φ j -> φ i < (φ j + 1) ^ 2 -> 2 * φ j < wB -> (forall j1 : int, 0 < φ j1 < φ j -> φ i < (φ j1 + 1) ^ 2 -> φ (rec i j1) ^ 2 <= φ i < (φ (rec i j1) + 1) ^ 2) -> φ (sqrt_step rec i j) ^ 2 <= φ i < (φ (sqrt_step rec i j) + 1) ^ 2.
proof: Proof. assert (Hp2: 0 < φ 2) by exact (refl_equal Lt). intros Hi Hj Hij H31 Hrec. unfold sqrt_step. case ltbP; rewrite div_spec. - intros hlt. assert (φ (j + i / j) = φ j + φ i/φ j) as hj. { rewrite add_spec, Zmod_small;rewrite div_spec; auto with zarith. } apply Hrec; rewrite lsr_spec, hj, to_Z_1; change (2 ^ 1) with 2. + split; [ | apply sqrt_test_false;auto with zarith]. replace (φ j + φ i/φ j) with (1 * 2 + ((φ j - 2) + φ i / φ j)) by ring. rewrite Z_div_plus_full_l; auto with zarith. assert (0 <= φ i/ φ j) by (apply Z_div_pos; auto with zarith). assert (0 <= (φ j - 2 + φ i / φ j) / 2) ; auto with zarith. apply Z.div_pos; [ | lia ]. case (Zle_lt_or_eq 1 φ j); auto with zarith; intros Hj1. rewrite <- Hj1, Zdiv_1_r; lia. + apply sqrt_main;auto with zarith. - split;[apply sqrt_test_true | ];auto with zarith. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63