proposition: Lemma egality_case_sum_of_four_squares : forall a b c d M, -M <= a < M -> -M <= b < M -> -M <= c < M -> -M <= d < M -> a * a + b * b + c * c + d * d = 4 * (M * M) -> ((a = -M) /\ (b = -M)) /\ ((c = -M) /\ (d = -M)).
proof: Proof. intros a b c d m Ba Bb Bc Bd E. assert (P : forall x, -m <= x < m -> -m <= x <= m) by (intros; lia). pose proof square_bound _ _ (P _ Ba). pose proof square_bound _ _ (P _ Bb). pose proof square_bound _ _ (P _ Bc). pose proof square_bound _ _ (P _ Bd). assert (Pm : 0 < m) by lia. cut ((Z.abs a = m /\ Z.abs b = m) /\ (Z.abs c = m /\ Z.abs d = m)). intros; lia. split; split; (rewrite <- (Z.abs_eq m); [ | auto with * ]); apply sqrt_eq_compat_abs; lia. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts