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

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

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