proposition: Lemma foursquare_prime_factor_decreasing : forall p, prime p -> forall m, (1 < m /\ m < p)%Z -> foursquare (m * p) -> sigT (fun n => ((0 < n /\ n < m)%Z * foursquare (n * p))%type).
proof: Proof. intros p Pp m (LBm, UBm) FSmp. assert (help0 : m <> 0); auto with *. assert (help1 : 0 < m); auto with *. destruct FSmp as (x1, (x2, (x3, (x4, Hx)))). pose (y1 := modsym x1 m). pose (y2 := modsym x2 m). pose (y3 := modsym x3 m). pose (y4 := modsym x4 m). assert (eqm1 : y1 ≡ x1 [m]) by apply modsym_eqm. assert (eqm2 : y2 ≡ x2 [m]) by apply modsym_eqm. assert (eqm3 : y3 ≡ x3 [m]) by apply modsym_eqm. assert (eqm4 : y4 ≡ x4 [m]) by apply modsym_eqm. assert (Dm : (m | y1 * y1 + y2 * y2 + y3 * y3 + y4 * y4)). apply divide_eqm; auto. rewrite eqm1, eqm2, eqm3, eqm4. rewrite <-Hx, divide_eqm; auto. apply Z.divide_factor_l. assert (Dmp : ~ (m | p)). intros D. eapply prime_div_false; eauto. destruct (Zdivide_inf _ _ Dm) as (r, Hr). exists r. split. assert (Pr : 0 <= r). apply Zmult_le_0_reg_r with m; auto with *. rewrite <- Hr. pose proof Zle_0_square y1. pose proof Zle_0_square y2. pose proof Zle_0_square y3. pose proof Zle_0_square y4. lia. assert (Nr : 0 <> r). intros Zr; subst. ring_simplify (0 * m) in Hr. assert (y0 : (y1 = 0 /\ y2 = 0) /\ (y3 = 0 /\ y4 = 0)). pose proof Zle_0_square y1. pose proof Zeq_0_square y1. pose proof Zle_0_square y2. pose proof Zeq_0_square y2. pose proof Zle_0_square y3. pose proof Zeq_0_square y3. pose proof Zle_0_square y4. pose proof Zeq_0_square y4. lia. apply Dmp. apply Zmult_divide_compat_rev_l with m; auto. rewrite Hx. repeat apply Zdivide_plus_r; apply Zdivide_square, divide_eqm; auto. rewrite <- eqm1; apply eq_eqm; tauto. rewrite <- eqm2; apply eq_eqm; tauto. rewrite <- eqm3; apply eq_eqm; tauto. rewrite <- eqm4; apply eq_eqm; tauto. assert (Lrm : r <= m). apply Zmult_le_reg_r with m; auto with *. rewrite <- Hr. apply Zmult_le_reg_r with 4; auto with *. ring_simplify. clear -help1 LBm. assert (B : forall x, 4 * (modsym x m) ^ 2 <= m ^2). clear -help1; intros x. pose proof modsym_bounds x m help1 as Bms. set (y := modsym x m); fold y in Bms; clearbody y. replace (4 * y ^ 2) with ((2 * y) ^ 2) by ring. apply Zbounding_square; auto. now auto with *. pose proof B x1 as Ey1; fold y1 in Ey1. pose proof B x2 as Ey2; fold y2 in Ey2. pose proof B x3 as Ey3; fold y3 in Ey3. pose proof B x4 as Ey4; fold y4 in Ey4. lia. assert (Nmr : r <> m). intros Emr; subst. assert (Eyi : (2 * - y1 = m /\ 2 * - y2 = m) /\ (2 * - y3 = m /\ 2 * - y4 = m)). assert (Eyi : (2 * y1 = - m /\ 2 * y2 = - m) /\ (2 * y3 = - m /\ 2 * y4 = - m)). apply egality_case_sum_of_four_squares; try (apply modsym_bounds; notzero). rewrite <- Hr; ring. lia. destruct Eyi as ((Ey1, Ey2), (Ey3, Ey4)). apply Dmp. apply Zmult_divide_compat_rev_l with m; auto. rewrite Hx. apply Zmult_divide_compat_rev_l with 4; notzero. rewrite <- divide_eqm; notzero. ring_simplify. assert (REW : forall x, 4 * x ^ 2 = (2 * x) * (2 * x)) by (intros; ring). repeat rewrite REW; clear REW. transitivity (m * m + m * m + m * m + m * m). cut (forall x y, 2 * -y = m -> y ≡ x [m] -> (2 * x) * (2 * x) ≡ m * m [4 * (m * m)]). intros HYP. repeat apply Zplus_eqm; (eapply HYP; [ | eassumption ]; eassumption). intros x y Ey Mxy. apply eqm_square_half; notzero. rewrite <- Ey at 2. apply eqm_mult_compat_l. rewrite <- Mxy. replace (- y) with (y + 2 * - y) by ring. rewrite Ey. rewrite eqm_minus_0. apply divide_eqm; notzero. exists (- 1); ring. apply divide_eqm; notzero. exists 1; ring. lia. assert (Erpm : (r * p) * (m * m) = (r * m) * (m * p)) by ring. rewrite Hx, <-Hr in Erpm. rewrite euler's_identity in Erpm. rem (y1 * x1 + y2 * x2 + y3 * x3 + y4 * x4) t1 Et1. rem (y1 * x2 - y2 * x1 - y3 * x4 + y4 * x3) t2 Et2. rem (y1 * x3 + y2 * x4 - y3 * x1 - y4 * x2) t3 Et3. rem (y1 * x4 - y2 * x3 + y3 * x2 - y4 * x1) t4 Et4. assert (D1 : (m | t1)). rewrite <- divide_eqm; auto; rewrite Et1. unfold y1, y2, y3, y4; repeat rewrite modsym_eqm. rewrite <-Hx, divide_eqm; auto. apply Z.divide_factor_l. assert (D2 : (m | t2)). rewrite <- divide_eqm; auto; rewrite Et2. unfold y1, y2, y3, y4; repeat rewrite modsym_eqm. try ring . red; f_equal; ring. assert (D3 : (m | t3)). rewrite <- divide_eqm; auto; rewrite Et3. unfold y1, y2, y3, y4; repeat rewrite modsym_eqm. red; f_equal; ring. assert (D4 : (m | t4)). rewrite <- divide_eqm; auto; rewrite Et4. unfold y1, y2, y3, y4; repeat rewrite modsym_eqm. red; f_equal; ring. exists (t1 / m); exists (t2 / m); exists (t3 / m); exists (t4 / m). apply Zmult_reg_r with (m * m). clear -help0; destruct m; auto; intro H; inversion H. rewrite Erpm. ring_simplify. cut (forall a, (m | a) -> (a / m) ^ 2 * m ^ 2 = a ^ 2). intros Q. do 4 (rewrite Q; auto). clear -help0. intros a D. destruct (Zdivide_inf m a D) as (k, E); subst. rewrite Z_div_mult_full; auto. ring. Defined.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts