m n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b + ↑d - (↑a + ↑c)
⊢ ↑n ∣ ↑d - ↑c
m n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : a + c ≡ b + d [MOD n]
⊢ c ≡ d [MOD n]
simp only [modEq_iff_dvd, Int.ofNat_add] at *
m n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b - ↑a + (↑d - ↑c)
⊢ ↑n ∣ ↑d - ↑c
m n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b + ↑d - (↑a + ↑c)
⊢ ↑n ∣ ↑d - ↑c
rw [add_sub_add_comm] at h₂
case h.e'_4
m n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b - ↑a + (↑d - ↑c)
⊢ ↑d - ↑c = ↑b - ↑a + (↑d - ↑c) - (↑b - ↑a)
m n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b - ↑a + (↑d - ↑c)
⊢ ↑n ∣ ↑d - ↑c
convert _root_.dvd_sub h₂ h₁ using 1
no goals
case h.e'_4
m n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b - ↑a + (↑d - ↑c)
⊢ ↑d - ↑c = ↑b - ↑a + (↑d - ↑c) - (↑b - ↑a)
rw [add_sub_cancel']