feat: gcd and coprime sub (#7051)

Co-authored-by: Moritz Firsching <firsching@google.com>

Author: mo271

Mathlib/Data/Nat/GCD/Basic.lean

@@ -6,6 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura
 import Mathlib.Algebra.GroupPower.Basic
 import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Data.Nat.Order.Lemmas
+import Mathlib.Tactic.NthRewrite
 
 #align_import data.nat.gcd.basic from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"
 
@@ -88,6 +89,30 @@ theorem gcd_self_add_right (m n : ℕ) : gcd m (m + n) = gcd m n := by
   rw [add_comm, gcd_add_self_right]
 #align nat.gcd_self_add_right Nat.gcd_self_add_right
 
+-- Lemmas where one argument consists of a subtraction of the other
+@[simp]
+theorem gcd_sub_self_left {m n : ℕ} (h : m ≤ n) : gcd (n - m) m = gcd n m := by
+  calc
+    gcd (n - m) m = gcd (n - m + m) m  := by rw [← gcd_add_self_left (n - m) m]
+                _ = gcd n m := by rw [Nat.sub_add_cancel h]
+
+@[simp]
+theorem gcd_sub_self_right {m n : ℕ} (h : m ≤ n) : gcd m (n - m) = gcd m n := by
+  rw [gcd_comm, gcd_sub_self_left h, gcd_comm]
+
+@[simp]
+theorem gcd_self_sub_left {m n : ℕ} (h : m ≤ n) : gcd (n - m) n = gcd m n := by
+  have := Nat.sub_add_cancel h
+  rw [gcd_comm m n, ← this, gcd_add_self_left (n - m) m]
+  have : gcd (n - m) n = gcd (n - m) m := by
+    nth_rw 2 [← Nat.add_sub_cancel' h]
+    rw [gcd_add_self_right, gcd_comm]
+  convert this
+
+@[simp]
+theorem gcd_self_sub_right {m n : ℕ} (h : m ≤ n) : gcd n (n - m) = gcd n m := by
+  rw [gcd_comm, gcd_self_sub_left h, gcd_comm]
+
 /-! ### `lcm` -/
 
 theorem lcm_dvd_mul (m n : ℕ) : lcm m n ∣ m * n :=
@@ -186,6 +211,22 @@ theorem coprime_mul_left_add_left (m n k : ℕ) : coprime (n * k + m) n ↔ copr
   rw [coprime, coprime, gcd_mul_left_add_left]
 #align nat.coprime_mul_left_add_left Nat.coprime_mul_left_add_left
 
+@[simp]
+theorem coprime_sub_self_left {m n : ℕ} (h : m ≤ n) : coprime (n - m) m ↔ coprime n m := by
+  rw [coprime, coprime, gcd_sub_self_left h]
+
+@[simp]
+theorem coprime_sub_self_right {m n : ℕ} (h : m ≤ n) : coprime m (n - m) ↔ coprime m n:= by
+  rw [coprime, coprime, gcd_sub_self_right h]
+
+@[simp]
+theorem coprime_self_sub_left {m n : ℕ} (h : m ≤ n) : coprime (n - m) n ↔ coprime m n := by
+  rw [coprime, coprime, gcd_self_sub_left h]
+
+@[simp]
+theorem coprime_self_sub_right {m n : ℕ} (h : m ≤ n) : coprime n (n - m) ↔ coprime n m := by
+  rw [coprime, coprime, gcd_self_sub_right h]
+
 @[simp]
 theorem coprime_pow_left_iff {n : ℕ} (hn : 0 < n) (a b : ℕ) :
     Nat.coprime (a ^ n) b ↔ Nat.coprime a b := by