case zero
n : ℕ
R : Type ?u.34539
inst✝ : Ring R
a b : ZMod Nat.zero
⊢ ↑(a + b) = ↑(if ↑Nat.zero ≤ ↑a + ↑b then a + b - ↑Nat.zero else a + b)

case succ
n : ℕ
R : Type ?u.34539
inst✝ : Ring R
n✝ : ℕ
a b : ZMod (Nat.succ n✝)
⊢ ↑(a + b) = ↑(if ↑(Nat.succ n✝) ≤ ↑a + ↑b then a + b - ↑(Nat.succ n✝) else a + b)
n✝ : ℕ
R : Type ?u.34539
inst✝ : Ring R
n : ℕ
a b : ZMod n
⊢ ↑(a + b) = ↑(if ↑n ≤ ↑a + ↑b then a + b - ↑n else a + b)
cases n
case succ
n : ℕ
R : Type ?u.34539
inst✝ : Ring R
n✝ : ℕ
a b : ZMod (Nat.succ n✝)
⊢ ↑(a + b) = ↑(if ↑(Nat.succ n✝) ≤ ↑a + ↑b then a + b - ↑(Nat.succ n✝) else a + b)
case succ
n : ℕ
R : Type ?u.34539
inst✝ : Ring R
n✝ : ℕ
a b : ZMod (Nat.succ n✝)
⊢ ↑(a + b) = ↑(if ↑(Nat.succ n✝) ≤ ↑a + ↑b then a + b - ↑(Nat.succ n✝) else a + b)
simp only [Fin.val_add_eq_ite, ← Int.ofNat_add, ← Int.ofNat_succ, Int.ofNat_le]
case succ.inl
n : ℕ
R : Type ?u.34539
inst✝ : Ring R
n✝ : ℕ
a b : ZMod (Nat.succ n✝)
h : ↑(Nat.succ n✝) ≤ ↑a + ↑b
⊢ ↑(a + b) = ↑(a + b - ↑(Nat.succ n✝))

case succ.inr
n : ℕ
R : Type ?u.34539
inst✝ : Ring R
n✝ : ℕ
a b : ZMod (Nat.succ n✝)
h : ¬↑(Nat.succ n✝) ≤ ↑a + ↑b
⊢ ↑(a + b) = ↑(a + b)
case succ
n : ℕ
R : Type ?u.34539
inst✝ : Ring R
n✝ : ℕ
a b : ZMod (Nat.succ n✝)
⊢ ↑(a + b) = ↑(if ↑(Nat.succ n✝) ≤ ↑a + ↑b then a + b - ↑(Nat.succ n✝) else a + b)
split_ifs with h
no goals
case zero
n : ℕ
R : Type ?u.34539
inst✝ : Ring R
a b : ZMod Nat.zero
⊢ ↑(a + b) = ↑(if ↑Nat.zero ≤ ↑a + ↑b then a + b - ↑Nat.zero else a + b)
simp
case succ.inl
n : ℕ
R : Type ?u.34539
inst✝ : Ring R
n✝ : ℕ
a b : ZMod (Nat.succ n✝)
h : ↑(Nat.succ n✝) ≤ ↑a + ↑b
⊢ ↑(a + b) = ↑(a + b - ↑(Nat.succ n✝))
case succ.inl
n : ℕ
R : Type ?u.34539
inst✝ : Ring R
n✝ : ℕ
a b : ZMod (Nat.succ n✝)
h : ↑(Nat.succ n✝) ≤ ↑a + ↑b
⊢ ↑(a + b) = ↑(a + b - ↑(Nat.succ n✝))
norm_cast
case succ.inl.e_a
n : ℕ
R : Type ?u.34539
inst✝ : Ring R
n✝ : ℕ
a b : ZMod (Nat.succ n✝)
h : ↑(Nat.succ n✝) ≤ ↑a + ↑b
⊢ a + b = a + b - ↑(Nat.succ n✝)
case succ.inl
n : ℕ
R : Type ?u.34539
inst✝ : Ring R
n✝ : ℕ
a b : ZMod (Nat.succ n✝)
h : ↑(Nat.succ n✝) ≤ ↑a + ↑b
⊢ ↑(a + b) = ↑(a + b - ↑(Nat.succ n✝))
congr
no goals
case succ.inl.e_a
n : ℕ
R : Type ?u.34539
inst✝ : Ring R
n✝ : ℕ
a b : ZMod (Nat.succ n✝)
h : ↑(Nat.succ n✝) ≤ ↑a + ↑b
⊢ a + b = a + b - ↑(Nat.succ n✝)
simp
no goals
case succ.inr
n : ℕ
R : Type ?u.34539
inst✝ : Ring R
n✝ : ℕ
a b : ZMod (Nat.succ n✝)
h : ¬↑(Nat.succ n✝) ≤ ↑a + ↑b
⊢ ↑(a + b) = ↑(a + b)
rfl