fix: added missing theorems in Algebra.Order.Archimedean (#2150)

[exists_unique_sub_zsmul_mem_Ico](https://leanprover-community.github.io/mathlib_docs/algebra/order/archimedean.html#exists_unique_sub_zsmul_mem_Ico) and [exists_unique_sub_zsmul_mem_Ioc](https://leanprover-community.github.io/mathlib_docs/algebra/order/archimedean.html#exists_unique_sub_zsmul_mem_Ioc) did not seem to get ported for some reason. They're used in Algebra/Order/ToIntervalMod, so let's fix this!

* [`algebra.order.archimedean`@`e001509c11c4d0f549d91d89da95b4a0b43c714f`..`6f413f3f7330b94c92a5a27488fdc74e6d483a78`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/archimedean?range=e001509c11c4d0f549d91d89da95b4a0b43c714f..6f413f3f7330b94c92a5a27488fdc74e6d483a78)

Mathlib/Algebra/Order/Archimedean.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 
 ! This file was ported from Lean 3 source module algebra.order.archimedean
-! leanprover-community/mathlib commit e001509c11c4d0f549d91d89da95b4a0b43c714f
+! leanprover-community/mathlib commit 6f413f3f7330b94c92a5a27488fdc74e6d483a78
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -82,6 +82,12 @@ theorem existsUnique_zsmul_near_of_pos' {a : α} (ha : 0 < a) (g : α) :
     existsUnique_zsmul_near_of_pos ha g
 #align exists_unique_zsmul_near_of_pos' existsUnique_zsmul_near_of_pos'
 
+theorem existsUnique_sub_zsmul_mem_Ico {a : α} (ha : 0 < a) (b c : α) :
+    ∃! m : ℤ, b - m • a ∈ Set.Ico c (c + a) := by
+  simpa only [mem_Ico, le_sub_iff_add_le, zero_add, add_comm c, sub_lt_iff_lt_add', add_assoc] using
+    existsUnique_zsmul_near_of_pos' ha (b - c)
+#align exists_unique_sub_zsmul_mem_Ico existsUnique_sub_zsmul_mem_Ico
+
 theorem existsUnique_add_zsmul_mem_Ico {a : α} (ha : 0 < a) (b c : α) :
     ∃! m : ℤ, b + m • a ∈ Set.Ico c (c + a) :=
   (Equiv.neg ℤ).bijective.existsUnique_iff.2 <| by
@@ -97,6 +103,13 @@ theorem existsUnique_add_zsmul_mem_Ioc {a : α} (ha : 0 < a) (b c : α) :
       existsUnique_zsmul_near_of_pos ha (c - b)
 #align exists_unique_add_zsmul_mem_Ioc existsUnique_add_zsmul_mem_Ioc
 
+theorem existsUnique_sub_zsmul_mem_Ioc {a : α} (ha : 0 < a) (b c : α) :
+    ∃! m : ℤ, b - m • a ∈ Set.Ioc c (c + a) :=
+  (Equiv.neg ℤ).bijective.existsUnique_iff.2 <| by
+    simpa only [Equiv.neg_apply, neg_zsmul, sub_neg_eq_add] using
+      existsUnique_add_zsmul_mem_Ioc ha b c
+#align exists_unique_sub_zsmul_mem_Ioc existsUnique_sub_zsmul_mem_Ioc
+
 end LinearOrderedAddCommGroup
 
 theorem exists_nat_gt [StrictOrderedSemiring α] [Archimedean α] (x : α) : ∃ n : ℕ, x < n :=