proposition: Lemma prime_dividing_sum_of_two_squares_plus_one : forall p, prime p -> 3 <= p -> {l : _ & {m : _ & { k | p * k = 1 + l * l + m * m /\ 2 * m < p /\ 2 * l < p /\ 0 < k /\ 0 <= l /\ 0 <= m /\ (0 < l \/ 0 < m)}}}.
proof: Proof. intros p Pp Op. pose (np := Z.abs_nat p). assert (p_odd : p mod 2 = 1) by (apply prime_odd; auto || lia). pose (s := fun x : Z => x * x). assert (s_pos : forall x, 0 <= s x). intros; unfold s; rewrite <- Z.abs_square. apply Zmult_le_0_compat; auto with *. assert (mod_pos : forall x, 0 <= x mod p). intros; apply Z_mod_lt; destruct Pp; lia. assert (hp_pos : 0 <= p / 2) by (apply Z_div_pos; lia). assert (autobound : forall i, (i < S (Z.abs_nat (p / 2)))%nat -> 2 * Z_of_nat i < p). intros i Li. apply inj_lt in Li. rewrite inj_S, inj_Zabs_nat, Z.abs_eq in Li; auto. apply odd_bound_1; auto. pose (FL := fun l => Z.abs_nat (s (Z_of_nat l) mod p)). pose (FM := fun m => Z.abs_nat ((-1 - s (Z_of_nat m)) mod p)). assert (IFL : injective (S (Z.abs_nat (p / 2))) FL). intros i j Li Lj E. unfold FL in E. apply Zabs_nat_inj in E; eauto. apply inj_eq_rev. apply (Zmod_sqrt_eq_compat p (Z_of_nat i) (Z_of_nat j)); auto with *. assert (IFM : injective (S (Z.abs_nat (p / 2))) FM). intros i j Li Lj E. unfold FM in E. apply inj_eq_rev. apply (Zmod_sqrt_eq_compat p (Z_of_nat i) (Z_of_nat j)); auto with *. apply Zabs_nat_inj in E; eauto. symmetry; apply eqm_minus_0. apply eqm_minus_0 in E. rewrite <- E. apply eq_eqm; unfold s; ring. assert (BFL : bounded (S (Z.abs_nat (p / 2))) (Z.abs_nat p) FL). intros i _. unfold FL. apply inj_lt_rev; do 2 rewrite inj_Zabs_nat. repeat rewrite Z.abs_eq; auto with *. apply Z_mod_lt; auto with *. assert (BFM : bounded (S (Z.abs_nat (p / 2))) (Z.abs_nat p) FM). intros i _. unfold FM. apply inj_lt_rev; do 2 rewrite inj_Zabs_nat. repeat rewrite Z.abs_eq; auto with *. apply Z_mod_lt; auto with *. assert (CL := count_image_injective (S (Z.abs_nat (p / 2))) np FL IFL BFL). assert (CM := count_image_injective (S (Z.abs_nat (p / 2))) np FM IFM BFM). remember (image FL (S (Z.abs_nat (p / 2)))) as L. remember (image FM (S (Z.abs_nat (p / 2)))) as M. destruct (count_drawers L M np) as (i, (Bi, (Li, Mi))). rewrite CL, CM. apply inj_lt_rev. rewrite inj_plus, inj_S, inj_Zabs_nat. rewrite Z.abs_eq; auto. unfold np; rewrite inj_Zabs_nat, Z.abs_eq; auto with *. unfold Z.succ. ring_simplify. pose proof Z_mult_div_bounds p 2. lia. rewrite HeqL in Li; rewrite HeqM in Mi. destruct (image_true _ _ _ Li) as (l, (Bl, Hl)). destruct (image_true _ _ _ Mi) as (m, (Bm, Hm)). exists (Z_of_nat l); exists (Z_of_nat m). unfold FL in Hl; unfold FM in Hm. clear HeqL CL HeqM CM Li Mi IFL IFM BFL BFM FL FM. subst. apply inj_eq in Hm; do 2 rewrite inj_Zabs_nat in Hm. do 2 rewrite Z.abs_eq in Hm; auto. symmetry in Hm; apply eqm_minus_0 in Hm. rewrite divide_eqm in Hm; notzero. pose proof s_pos (Z_of_nat l). pose proof s_pos (Z_of_nat m). destruct (Zdivide_inf _ _ Hm) as (k, Hk). exists k. assert (0 < k * p) by lia. assert (0 < k) by (apply Zmult_lt_0_reg_r with p; assumption || lia). assert (3 <= k * p). replace 3 with (1 * 3) by reflexivity. apply Zmult_le_compat; lia. repeat split; auto with *. rewrite Zmult_comm, <- Hk. unfold s; ring. rem (Z_of_nat l) lz Elz. rem (Z_of_nat m) mz Emz. cut (0 <> lz \/ 0 <> mz); [ lia | ]. cut (0 <> s lz \/ 0 <> s mz). cut (forall a, 0 <> s a -> 0 <> a). intros Hyp [?|?]; [left|right]; apply Hyp; auto. clear; intros [] H; tauto || zify; auto with *. lia. Defined.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts