Theorem: Imo1959P2.sqrt_two_mul_sub_one_le_one (Compfiles/Imo1959P2.lean)

State before:
x A : ℝ
⊢ √(2 * x - 1) ≤ 1 ↔ x ≤ 1
Tactic:
simp [sqrt_le_iff, ← two_mul]
State after:
no goals