case zero
inst✝ : NeZero Nat.zero
a b : ZMod Nat.zero
⊢ val (a + b) = (val a + val b) % Nat.zero

case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a b : ZMod (Nat.succ n✝)
⊢ val (a + b) = (val a + val b) % Nat.succ n✝
n : ℕ
inst✝ : NeZero n
a b : ZMod n
⊢ val (a + b) = (val a + val b) % n
cases n
no goals
case zero
inst✝ : NeZero Nat.zero
a b : ZMod Nat.zero
⊢ val (a + b) = (val a + val b) % Nat.zero
cases NeZero.ne 0 rfl
no goals
case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a b : ZMod (Nat.succ n✝)
⊢ val (a + b) = (val a + val b) % Nat.succ n✝
apply Fin.val_add