proposition: Lemma sqrt_main_trick j k: 0 <= j -> 0 <= k -> (j * k) + j <= ((j + k)/2 + 1) ^ 2.
proof: Proof. intros Hj; generalize Hj k; pattern j; apply natlike_ind; auto; clear k j Hj. - intros _ k Hk; repeat rewrite Zplus_0_l. apply Zmult_le_0_compat; generalize (Z_div_pos k 2); auto with zarith. - intros j Hj Hrec _ k Hk; pattern k; apply natlike_ind; auto; clear k Hk. + rewrite -> Zmult_0_r, Zplus_0_r, Zplus_0_l. generalize (sqr_pos (Z.succ j / 2)) (quotient_by_2 (Z.succ j)); unfold Z.succ. rewrite Z.pow_2_r, Zmult_plus_distr_l; repeat rewrite Zmult_plus_distr_r. auto with zarith. + intros k Hk _. replace ((Z.succ j + Z.succ k) / 2) with ((j + k)/2 + 1). * generalize (Hrec Hj k Hk) (quotient_by_2 (j + k)). unfold Z.succ; repeat rewrite Z.pow_2_r; repeat rewrite Zmult_plus_distr_l; repeat rewrite Zmult_plus_distr_r. repeat rewrite Zmult_1_l; repeat rewrite Zmult_1_r. auto with zarith. * rewrite -> Zplus_comm, <- Z_div_plus_full_l; auto with zarith. apply f_equal2; auto with zarith. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63