no goals
m n a✝ b✝ c✝ d a b c : ℕ
hca : c ∣ a
h : c = 0
⊢ (a + b) / c = a / c + b / c
simp [h]
m n a✝ b✝ c✝ d a b c : ℕ
hca : c ∣ a
h : ¬c = 0
⊢ b % c < c
m n a✝ b✝ c✝ d a b c : ℕ
hca : c ∣ a
h : ¬c = 0
⊢ a % c + b % c < c
rw [Nat.mod_eq_zero_of_dvd hca, zero_add]
no goals
m n a✝ b✝ c✝ d a b c : ℕ
hca : c ∣ a
h : ¬c = 0
⊢ b % c < c
exact Nat.mod_lt _ (pos_iff_ne_zero.mpr h)