Theorem: HTPI.le_nonzero_prod_right (HTPILib/Chap7.lean)

State before:
a b : ℕ
h : a * b ≠ 0
⊢ b ≤ a * b
Tactic:
rewrite [mul_comm]
State after:
a b : ℕ
h : a * b ≠ 0
⊢ b ≤ b * a

State before:
a b : ℕ
h : a * b ≠ 0
⊢ b ≤ b * a
Tactic:
rewrite [mul_comm] at h
State after:
a b : ℕ
h : b * a ≠ 0
⊢ b ≤ b * a

State before:
a b : ℕ
h : b * a ≠ 0
⊢ b ≤ b * a
Tactic:
show b ≤ b * a from le_nonzero_prod_left h
State after:
no goals