have PROD_NONZERO: shapeProd shape > 0 := flat.bound_gt_zero
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
⊢ n > 0
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ n > 0