convert Nat.cast_le (α := ℚ)
C : Type u_1
J : Type u_2
r : C → J → Prop
a b k : ℕ
ha : 0 < a
hb : 0 < b
⊢ (↑b - 1) * ↑a ≤ ↑k * (2 * ↑b) ↔ (b - 1) * a ≤ k * (2 * b)
case h.e'_1.h.e'_3
C : Type u_1
J : Type u_2
r : C → J → Prop
a b k : ℕ
ha : 0 < a
hb : 0 < b
⊢ (↑b - 1) * ↑a = ↑((b - 1) * a)

case h.e'_1.h.e'_4
C : Type u_1
J : Type u_2
r : C → J → Prop
a b k : ℕ
ha : 0 < a
hb : 0 < b
⊢ ↑k * (2 * ↑b) = ↑(k * (2 * b))