calc
  a * p + b < a * p + p    := by simp [hb]
  _         = (a + 1) * p  := by simp [add_mul]
  _         ≤ 2 * (a' * p) := by simp [←mul_assoc]; exact mul_le_mul_right (lt_iff_succ_le.mp ha)
case refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a p b : M
pos : 0 < a
pp : Pow2 p
hb : b < p
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
ha : a < 2 * a'
hp' : p ≤ p
Hp : Exponential (log p) p
hp : p < 2 * p
⊢ a * p + b < 2 * (a' * p)
no goals