Theorem: Nat.succ_gt_zero (MLIR/Util/KDTensor.lean)

State before:
n : ℕ
⊢ succ n > 0
Tactic:
simp [GT.gt]
State after:
no goals