cases bound
bound : ℕ
flat : TensorFlatIndex bound
BOUND_NONZERO : bound ≠ 0
⊢ bound > 0
case zero
flat : TensorFlatIndex Nat.zero
BOUND_NONZERO : Nat.zero ≠ 0
⊢ Nat.zero > 0

case succ
n✝ : ℕ
flat : TensorFlatIndex (Nat.succ n✝)
BOUND_NONZERO : Nat.succ n✝ ≠ 0
⊢ Nat.succ n✝ > 0