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

State before:
n a b : ℕ
hab : a ≤ b
⊢ a * n / b ≤ n
Tactic:
cases b with
| zero => simp
| succ b =>
  conv => rhs; rw [← Nat.mul_div_right n (Nat.zero_lt_succ b)]
  apply Nat.div_le_div_right
  exact Nat.mul_le_mul_right _ hab
State after:
no goals

State before:
case zero
n a : ℕ
hab : a ≤ Nat.zero
⊢ a * n / Nat.zero ≤ n
Tactic:
simp
State after:
no goals

State before:
case succ
n a b : ℕ
hab : a ≤ Nat.succ b
⊢ a * n / Nat.succ b ≤ n
Tactic:
conv => rhs; rw [← Nat.mul_div_right n (Nat.zero_lt_succ b)]
State after:
case succ
n a b : ℕ
hab : a ≤ Nat.succ b
⊢ a * n / Nat.succ b ≤ Nat.succ b * n / Nat.succ b

State before:
case succ
n a b : ℕ
hab : a ≤ Nat.succ b
⊢ a * n / Nat.succ b ≤ Nat.succ b * n / Nat.succ b
Tactic:
apply Nat.div_le_div_right
State after:
case succ.h
n a b : ℕ
hab : a ≤ Nat.succ b
⊢ a * n ≤ Nat.succ b * n

State before:
case succ.h
n a b : ℕ
hab : a ≤ Nat.succ b
⊢ a * n ≤ Nat.succ b * n
Tactic:
exact Nat.mul_le_mul_right _ hab
State after:
no goals