Theorem: IMOSL.IMO2012A7.le_max_one_sq (IMOSLLean4/IMO2012/A7/A7PiRing.lean)

State before:
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
⊢ a ≤ max 1 (a ^ 2)
Tactic:
apply (le_abs_self a).trans
State after:
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
⊢ |a| ≤ max 1 (a ^ 2)

State before:
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
⊢ |a| ≤ max 1 (a ^ 2)
Tactic:
rw [← sq_abs, le_max_iff]
State after:
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
⊢ |a| ≤ 1 ∨ |a| ≤ |a| ^ 2

State before:
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
⊢ |a| ≤ 1 ∨ |a| ≤ |a| ^ 2
Tactic:
exact (le_total |a| 1).imp_right λ h ↦ le_self_pow h (Nat.succ_ne_zero 1)
State after:
no goals