@[simp]

theorem Nat.dvd_add_mul_self {a b c : ℕ} : a ∣ b + c * a ↔ a ∣ b

@[simp]

theorem Nat.dvd_add_self_mul {a b c : ℕ} : a ∣ b + a * c ↔ a ∣ b

@[simp]

theorem Nat.dvd_mul_self_add {a b c : ℕ} : a ∣ b * a + c ↔ a ∣ c

@[simp]

theorem Nat.dvd_self_mul_add {a b c : ℕ} : a ∣ a * b + c ↔ a ∣ c

@[simp]

theorem Nat.dvd_sub_iff_right' {a b c : ℕ} (hab : a ∣ b) : a ∣ b - c ↔ a ∣ c ∨ b ≤ c

@[simp]

theorem Nat.dvd_sub_iff_left' {a b c : ℕ} (hac : a ∣ c) : a ∣ b - c ↔ a ∣ b ∨ b ≤ c

@[simp]

theorem Nat.dvd_sub_mul_self {a b c : ℕ} : a ∣ b - c * a ↔ a ∣ b ∨ b ≤ c * a

@[simp]

theorem Nat.dvd_sub_self_mul {a b c : ℕ} : a ∣ b - a * c ↔ a ∣ b ∨ b ≤ c * a

@[simp]

theorem Nat.dvd_mul_self_sub {a b c : ℕ} : a ∣ b * a - c ↔ a ∣ c ∨ b * a ≤ c

@[simp]

theorem Nat.dvd_self_mul_sub {a b c : ℕ} : a ∣ a * b - c ↔ a ∣ c ∨ b * a ≤ c