cases b.natNorm
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
⊢ natNorm b = 0
case zero
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
⊢ Nat.zero = 0

case succ
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
n✝ : ℕ
⊢ Nat.succ n✝ = 0