proposition: Lemma sqrt_init i: 1 < i -> i < (i/2 + 1) ^ 2.
proof: Proof. intros Hi. assert (H1: 0 <= i - 2) by auto with zarith. assert (H2: 1 <= (i / 2) ^ 2); auto with zarith. { replace i with (1* 2 + (i - 2)); auto with zarith. rewrite Z.pow_2_r, Z_div_plus_full_l; [|auto with zarith]. generalize (sqr_pos ((i - 2)/ 2)) (Z_div_pos (i - 2) 2). rewrite Zmult_plus_distr_l; repeat rewrite Zmult_plus_distr_r. auto with zarith. } generalize (quotient_by_2 i). rewrite -> Z.pow_2_r in H2 |- *; repeat (rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r || rewrite Zmult_1_l || rewrite Zmult_1_r). auto with zarith. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63