Theorem: Real.pow_two_le_pow_two (CvxLean/Lib/Math/Data/Real.lean)

State before:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x ^ 2 ≤ y ^ 2 ↔ x ≤ y
Tactic:
rw [rpow_two, rpow_two, sq_le_sq, abs_of_nonneg hx, abs_of_nonneg hy]
State after:
no goals