case zero
m n l : ℕ
⊢ (m + n) % zero = if zero ≤ m % zero + n % zero then m % zero + n % zero - zero else m % zero + n % zero

case succ
m n l n✝ : ℕ
⊢ (m + n) % succ n✝ =
    if succ n✝ ≤ m % succ n✝ + n % succ n✝ then m % succ n✝ + n % succ n✝ - succ n✝ else m % succ n✝ + n % succ n✝
m n k l : ℕ
⊢ (m + n) % k = if k ≤ m % k + n % k then m % k + n % k - k else m % k + n % k
cases k
case succ
m n l n✝ : ℕ
⊢ (m + n) % succ n✝ =
    if succ n✝ ≤ m % succ n✝ + n % succ n✝ then m % succ n✝ + n % succ n✝ - succ n✝ else m % succ n✝ + n % succ n✝
case zero
m n l : ℕ
⊢ (m + n) % zero = if zero ≤ m % zero + n % zero then m % zero + n % zero - zero else m % zero + n % zero

case succ
m n l n✝ : ℕ
⊢ (m + n) % succ n✝ =
    if succ n✝ ≤ m % succ n✝ + n % succ n✝ then m % succ n✝ + n % succ n✝ - succ n✝ else m % succ n✝ + n % succ n✝
simp [mod_zero]
case succ
m n l n✝ : ℕ
⊢ (m % succ n✝ + n % succ n✝) % succ n✝ =
    if succ n✝ ≤ m % succ n✝ + n % succ n✝ then m % succ n✝ + n % succ n✝ - succ n✝ else m % succ n✝ + n % succ n✝
case succ
m n l n✝ : ℕ
⊢ (m + n) % succ n✝ =
    if succ n✝ ≤ m % succ n✝ + n % succ n✝ then m % succ n✝ + n % succ n✝ - succ n✝ else m % succ n✝ + n % succ n✝
rw [Nat.add_mod]
case succ.inl
m n l n✝ : ℕ
h : succ n✝ ≤ m % succ n✝ + n % succ n✝
⊢ (m % succ n✝ + n % succ n✝) % succ n✝ = m % succ n✝ + n % succ n✝ - succ n✝

case succ.inr
m n l n✝ : ℕ
h : ¬succ n✝ ≤ m % succ n✝ + n % succ n✝
⊢ (m % succ n✝ + n % succ n✝) % succ n✝ = m % succ n✝ + n % succ n✝
case succ
m n l n✝ : ℕ
⊢ (m % succ n✝ + n % succ n✝) % succ n✝ =
    if succ n✝ ≤ m % succ n✝ + n % succ n✝ then m % succ n✝ + n % succ n✝ - succ n✝ else m % succ n✝ + n % succ n✝
split_ifs with h
case succ.inl
m n l n✝ : ℕ
h : succ n✝ ≤ m % succ n✝ + n % succ n✝
⊢ m % succ n✝ + n % succ n✝ - succ n✝ < succ n✝
case succ.inl
m n l n✝ : ℕ
h : succ n✝ ≤ m % succ n✝ + n % succ n✝
⊢ (m % succ n✝ + n % succ n✝) % succ n✝ = m % succ n✝ + n % succ n✝ - succ n✝
rw [Nat.mod_eq_sub_mod h, Nat.mod_eq_of_lt]
no goals
case succ.inl
m n l n✝ : ℕ
h : succ n✝ ≤ m % succ n✝ + n % succ n✝
⊢ m % succ n✝ + n % succ n✝ - succ n✝ < succ n✝
exact
  (tsub_lt_iff_right h).mpr (Nat.add_lt_add (m.mod_lt (zero_lt_succ _))
    (n.mod_lt (zero_lt_succ _)))
no goals
case succ.inr
m n l n✝ : ℕ
h : ¬succ n✝ ≤ m % succ n✝ + n % succ n✝
⊢ (m % succ n✝ + n % succ n✝) % succ n✝ = m % succ n✝ + n % succ n✝
exact Nat.mod_eq_of_lt (lt_of_not_ge h)