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

State before:
a b x : ℕ
H : a < b
XNEQ0 : 0 < x
⊢ a * x < b * x
Tactic:
sorry_arith
State after:
no goals