Theorem: Misc.Nat.le_mul_of_pos_left (LeanSAT/Util/Misc.lean)

State before:
n m : Nat
h : 0 < n
⊢ m ≤ n * m
Tactic:
conv =>
  lhs
  rw [← Nat.one_mul m]
State after:
n m : Nat
h : 0 < n
⊢ 1 * m ≤ n * m

State before:
n m : Nat
h : 0 < n
⊢ 1 * m ≤ n * m
Tactic:
exact Nat.mul_le_mul_right _ $ Nat.succ_le_of_lt h
State after:
no goals