case zero
a b : ZMod Nat.zero
⊢ val (a * b) = val a * val b % Nat.zero

case succ
n✝ : ℕ
a b : ZMod (Nat.succ n✝)
⊢ val (a * b) = val a * val b % Nat.succ n✝
n : ℕ
a b : ZMod n
⊢ val (a * b) = val a * val b % n
cases n
case zero
a b : ZMod Nat.zero
⊢ val (a * b) = val a * val b
case zero
a b : ZMod Nat.zero
⊢ val (a * b) = val a * val b % Nat.zero
rw [Nat.mod_zero]
no goals
case zero
a b : ZMod Nat.zero
⊢ val (a * b) = val a * val b
apply Int.natAbs_mul
no goals
case succ
n✝ : ℕ
a b : ZMod (Nat.succ n✝)
⊢ val (a * b) = val a * val b % Nat.succ n✝
apply Fin.val_mul