m n k l a b : ℕ
h : a / 2 < a - b
⊢ b * 2 ≤ a
m n k l a b : ℕ
h : a / 2 < a - b
⊢ b ≤ a / 2
rw [Nat.le_div_iff_mul_le two_pos]
m n k l a b : ℕ
h✝ : a < a * 2 - b * 2
h : a + b * 2 < a + a
⊢ b * 2 ≤ a
m n k l a b : ℕ
h : a / 2 < a - b
⊢ b * 2 ≤ a
rw [Nat.div_lt_iff_lt_mul two_pos, Nat.mul_sub_right_distrib, lt_tsub_iff_right, mul_two a] at h
no goals
m n k l a b : ℕ
h✝ : a < a * 2 - b * 2
h : a + b * 2 < a + a
⊢ b * 2 ≤ a
exact le_of_lt (Nat.lt_of_add_lt_add_left h)