feat: Data/Int/ModEq add theorem modEq_sub_fac, compliment modEq_add_…

…fac (#6040)

Easy of use function to compliment modEq_add_fac, the statement that :

a = b [ZMOD n] implies a - c * n = b [ZMOD n]

Mathlib/Data/Int/ModEq.lean

@@ -286,6 +286,10 @@ theorem modEq_add_fac {a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) : a + n *
     _ ≡ b [ZMOD n] := by rw [add_zero]
 #align int.modeq_add_fac Int.modEq_add_fac
 
+theorem modEq_sub_fac {a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) : a - n * c ≡ b [ZMOD n] := by
+  convert Int.modEq_add_fac (-c) ha using 1
+  ring
+
 theorem modEq_add_fac_self {a t n : ℤ} : a + n * t ≡ a [ZMOD n] :=
   modEq_add_fac _ ModEq.rfl
 #align int.modeq_add_fac_self Int.modEq_add_fac_self