Theorem: mulRightLeOfLeOne (FromTheBook/Ch02/Bertrand/CentralBinom.lean)

State before:
x y z : ℕ
h1 : x ≤ 1
h : y ≤ z
⊢ x * y ≤ z
Tactic:
rw [← Nat.one_mul z]
State after:
x y z : ℕ
h1 : x ≤ 1
h : y ≤ z
⊢ x * y ≤ 1 * z

State before:
x y z : ℕ
h1 : x ≤ 1
h : y ≤ z
⊢ x * y ≤ 1 * z
Tactic:
apply Nat.mul_le_mul h1 h
State after:
no goals