Update S03_Building_the_Gaussian_Integers.lean

No longer necessary.
avigad · Jan 6, 2025 · 1988747 · 1988747
1 parent 4ad0aeb
commit 1988747
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean b/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean
@@ -390,7 +390,6 @@ theorem abs_mod'_le (a b : ℤ) (h : 0 < b) : |mod' a b| ≤ b / 2 := by
   have := Int.emod_lt_of_pos (a + b / 2) h
   have := Int.ediv_add_emod b 2
   have := Int.emod_lt_of_pos b zero_lt_two
-  revert this; intro this -- FIXME, this should not be needed
   linarith
 -- QUOTE.