m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
⊢ (a + b) % c + a % c + b % c + c * ((a + b) / c) =
    (a + b) % c + a % c + b % c + c * (a / c + b / c + if c ≤ a % c + b % c then 1 else 0)
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
⊢ (a + b) / c = a / c + b / c + if c ≤ a % c + b % c then 1 else 0
rw [← mul_right_inj' hc0.ne', ← @add_left_cancel_iff _ _ _ ((a + b) % c + a % c + b % c)]
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
⊢ (a + b) % c + c * ((a + b) / c) + a % c + b % c =
    (a % c + c * (a / c) + (b % c + c * (b / c)) + c * if c ≤ a % c + b % c then 1 else 0) + (a + b) % c
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
⊢ (a + b) % c + a % c + b % c + c * ((a + b) / c) =
    (a + b) % c + a % c + b % c + c * (a / c + b / c + if c ≤ a % c + b % c then 1 else 0)
suffices
  (a + b) % c + c * ((a + b) / c) + a % c + b % c =
    (a % c + c * (a / c) + (b % c + c * (b / c)) + c * if c ≤ a % c + b % c then 1 else 0) +
      (a + b) % c
  by simpa only [mul_add, add_comm, add_left_comm, add_assoc]
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
⊢ a + (b + (a % c + b % c)) = (a + b + if c ≤ a % c + b % c then c * 1 else c * 0) + (a + b) % c
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
⊢ (a + b) % c + c * ((a + b) / c) + a % c + b % c =
    (a % c + c * (a / c) + (b % c + c * (b / c)) + c * if c ≤ a % c + b % c then 1 else 0) + (a + b) % c
rw [mod_add_div, mod_add_div, mod_add_div, mul_ite, add_assoc, add_assoc]
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
⊢ a + (b + ((a + b) % c + if c ≤ a % c + b % c then c else 0)) =
    (a + b + if c ≤ a % c + b % c then c * 1 else c * 0) + (a + b) % c
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
⊢ a + (b + (a % c + b % c)) = (a + b + if c ≤ a % c + b % c then c * 1 else c * 0) + (a + b) % c
conv_lhs => rw [← add_mod_add_ite]
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
⊢ a + (b + ((a + b) % c + if c ≤ a % c + b % c then c else 0)) =
    (a + b + if c ≤ a % c + b % c then c else 0) + (a + b) % c
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
⊢ a + (b + ((a + b) % c + if c ≤ a % c + b % c then c else 0)) =
    (a + b + if c ≤ a % c + b % c then c * 1 else c * 0) + (a + b) % c
simp
no goals
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
⊢ a + (b + ((a + b) % c + if c ≤ a % c + b % c then c else 0)) =
    (a + b + if c ≤ a % c + b % c then c else 0) + (a + b) % c
ac_rfl
no goals
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
this :
  (a + b) % c + c * ((a + b) / c) + a % c + b % c =
    (a % c + c * (a / c) + (b % c + c * (b / c)) + c * if c ≤ a % c + b % c then 1 else 0) + (a + b) % c
⊢ (a + b) % c + a % c + b % c + c * ((a + b) / c) =
    (a + b) % c + a % c + b % c + c * (a / c + b / c + if c ≤ a % c + b % c then 1 else 0)
simpa only [mul_add, add_comm, add_left_comm, add_assoc]