case zero
inst✝ : NeZero Nat.zero
a : ZMod Nat.zero
⊢ val a < Nat.zero

case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a : ZMod (Nat.succ n✝)
⊢ val a < Nat.succ n✝
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ val a < n
cases n
no goals
case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a : ZMod (Nat.succ n✝)
⊢ val a < Nat.succ n✝
exact Fin.is_lt a
no goals
case zero
inst✝ : NeZero Nat.zero
a : ZMod Nat.zero
⊢ val a < Nat.zero
cases NeZero.ne 0 rfl