Theorem: TensorFlatIndex.bound_zero_absurd (MLIR/Util/KDTensor.lean)

State before:
flat : TensorFlatIndex 0
⊢ False
Tactic:
have H_INBOUND := flat.h_ix_inbound
State after:
flat : TensorFlatIndex 0
H_INBOUND : flat.ix < 0
⊢ False

State before:
flat : TensorFlatIndex 0
H_INBOUND : flat.ix < 0
⊢ False
Tactic:
simp [Nat.not_lt_zero] at H_INBOUND
State after:
no goals