proposition: Lemma foursquare_prime : forall p, prime p -> foursquare p.
proof: Proof. intros p Pp. destruct (Z.eq_dec p 2) as [E | E]. do 2 exists 1%Z; do 2 exists 0%Z; auto. assert (3 <= p) as Op by (pose proof (prime_ge_2 p Pp); lia); clear E. pose (fs_mult := fun p m => prod (foursquare (Z_of_nat (S m) * p)) (Z_of_nat (S m) < p)). assert (sigT (fs_mult p)) as Hm. destruct (prime_dividing_sum_of_two_squares_plus_one p Pp Op) as (l, (m, (k, (Ep, (Bm, (Bl, (Pk, Plm))))))). assert (tech1 : Z_of_nat (S (Z.abs_nat (k - 1))) = k). rewrite inj_S, inj_Zabs_nat, Z.abs_eq; [ | lia ]; auto with *. exists (Z.abs_nat (k - 1)); split. exists 0%Z; exists 1%Z; exists l; exists m. transitivity (p * k). rewrite tech1; ring. rewrite Ep; auto. rewrite tech1; clear tech1. apply Zmult_lt_reg_r with (4 * p); [ auto with * | ]. replace (p * (4 * p)) with (2 * (p * p) + 2 * (p * p)) by ring. replace (k * (4 * p)) with (4 * (p * k)) by ring. rewrite Ep. assert (tech2 : forall a b, 0 < a -> 2 * a < b -> 4 * a * a + 4 < b * b). clear; intros a b Pa LT. assert (LE : 2 * a + 1 <= b) by lia. assert (Pda : 0 <= 2 * a + 1) by lia. assert (LE2 := Zmult_le_compat _ _ _ _ LE LE Pda Pda). eapply Z.lt_le_trans; [ | apply LE2 ]. ring_simplify. lia. assert (tech3 : forall a b, 0 <= a -> 2 * a < b -> 4 * a * a < b * b). clear; intros a b Pa LT. assert (LE : 2 * a + 1 <= b) by lia. assert (Pda : 0 <= 2 * a + 1) by lia. assert (LE2 := Zmult_le_compat _ _ _ _ LE LE Pda Pda). eapply Z.lt_le_trans; [ | apply LE2 ]. ring_simplify. lia. assert (p2_pos : 0 < p * p). transitivity (1 * p). lia. apply Zmult_lt_compat_r; lia. rem (l * l) ll Ell. rem (m * m) mm Emm. rem (p * p) pp Epp. destruct Plm as (NNl, (NNm, [Pl | Pm])). specialize (tech2 _ p Pl Bl). specialize (tech3 _ p NNm Bm). rewrite <- Zmult_assoc, <-Ell, <-Emm, <-Epp in *. clear -tech2 tech3 p2_pos. ring_simplify. lia. specialize (tech2 _ p Pm Bm). specialize (tech3 _ p NNl Bl). rewrite <- Zmult_assoc, <-Ell, <-Emm, <-Epp in *. clear -tech2 tech3 p2_pos. ring_simplify. lia. clear Op. destruct Hm as (m, Hm). generalize p Pp m Hm; clear Hm m Pp p. intros p Pp m. refine (lt_wf_rect m (fun n => fs_mult p n -> foursquare p) _); clear m. intros [|m] IH (FSm, UBm). destruct p; assumption. assert (LBm : 1 < Z_of_nat (S (S m))) by lia. destruct (foursquare_prime_factor_decreasing p Pp _ (conj LBm UBm) FSm) as (n, ((LBn, UBn), FSn)). apply IH with (Z.abs_nat (n - 1)). unfold ltof. lia. unfold fs_mult. rewrite inj_S, inj_Zabs_nat, Z.abs_eq; auto with *; unfold Z.succ. replace (n - 1 + 1) with n by ring. split; auto; lia. Defined.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts