rw [div_mul_comm, mul_one]
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4 < (C₁ / (C₂ * 2)) ^ 4
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ (C₁ / (C₂ * 2)) ^ 4 / 2 < (C₁ / (C₂ * 2)) ^ 4