work in progress on thue's lemma

Compfiles/Bulgaria1998P11.lean

@@ -222,6 +222,70 @@ lemma too_good_to_be_true (n l : ℕ)
 lemma Thue's_lemma (a m : ℤ) : ∃ (x y : ℤ),  a * x + y ≡ 0 [ZMOD m] ∧ 0 < x ^ 2 ∧ x ^ 2 < m ∧ y ^ 2 ≤ m :=
   sorry
 
+lemma thue
+    {n : ℕ} (hm : 1 < n)
+    (a : ZMod n)
+    (hn : Prime n) :
+    ∃ (x y : ℤ), x = a * y ∧ 0 < x ^ 2 ∧ x ^ 2 < n ∧ y ^ 2 < n := by
+  -- https://services.artofproblemsolving.com/download.php?id=YXR0YWNobWVudHMvMy8yL2QzYjEzOGM0ODE3YzYwZGU4NGFmOTEwZDc0ZGNhODRjOGMyMzZlLnBkZg==&rn=dGh1ZS12NC5wZGY=
+
+  -- let r = ⌊√n⌋, i.e. r is the unique integer for which
+  -- r² ≤ n < (r + 1)².
+  let r := Nat.sqrt n
+
+  -- The number of pairs (x,y) so that 0 ≤ x,y ≤ r is (r + 1)² which
+  -- is greater than n.
+
+  --
+  -- Therefore there must be two different pairs (x₁, y₁) and (x₂, y₂)
+  -- such that
+  --     x₁ - ay₁ = x₂ - ay₂ (mod n)
+  --     i.e.
+  --     x₁ - x₂ = a(y₁ - y₂) (mod n)
+  --
+
+  let D := Fin (r + 1) × Fin (r + 1)
+  let f : D → ZMod n := fun ⟨x,y⟩ ↦ (x.val : ZMod n) - a * (y.val : ZMod n)
+  have cardD : Fintype.card D = (r + 1)^2 := by
+    unfold_let D
+    rw [sq, Fintype.card_prod, Fintype.card_fin]
+
+  have : NeZero n := NeZero.of_gt hm
+  have cardZ : Fintype.card (ZMod n) = n := ZMod.card n
+
+  have hDZ : Fintype.card (ZMod n) < Fintype.card D := by
+    rw [cardD, cardZ]
+    exact Nat.lt_succ_sqrt' n
+
+  obtain ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩, hxyn, hxy⟩ :=
+    Fintype.exists_ne_map_eq_of_card_lt f hDZ
+  dsimp [f] at hxy
+  have hxy' : ↑↑x₁ - ↑↑x₂ = a * ↑↑y₁ - a * ↑↑y₂ :=
+    sub_eq_sub_iff_sub_eq_sub.mp hxy
+  use (x₁ : ℤ) - (x₂ : ℤ)
+  use (y₁ : ℤ) - (y₂ : ℤ)
+  have h3 : (((x₁ : ℕ): ℤ) : ZMod n) - (((x₂ : ℕ): ℤ) : ZMod n) =
+            (((((x₁ : ℕ): ℤ) -((x₂ : ℕ): ℤ)) : ℤ) : ZMod n) := by
+    norm_cast
+
+  constructor
+  · have h1 : ((x₁ : ℕ): ZMod n) = (((x₁ : ℕ): ℤ) : ZMod n)  := by
+      norm_cast
+    have h2 : ((x₂ : ℕ): ZMod n) = (((x₂ : ℕ): ℤ) : ZMod n)  := by
+      norm_cast
+    rw [h1, h2, h3] at hxy'
+    rw [hxy']
+    rw [←mul_sub]
+    congr 1
+    norm_cast
+  refine ⟨?_, ?_, ?_⟩
+  · by_contra! H
+    replace H : (((x₁:ℕ):ZMod n) - ↑↑x₂) ^ 2 = 0 := by
+      sorry
+    sorry
+  · sorry
+  · sorry
+
 lemma mod_z_of_mod_n {a b m : ℕ} (h : a ≡ b [MOD m]) : a ≡ b [ZMOD m] := by
   dsimp [Int.ModEq]
   rw[show a % m = @Nat.cast ℤ _ (a % m) by norm_num]