ι : Type ?u.187185
α : Type u_1
β : Type ?u.187191
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
a2 : 2 ≤ a
⊢ 2⁻¹ ≤ 1 - 1 / a
ι : Type ?u.187185
α : Type u_1
β : Type ?u.187191
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
a2 : 2 ≤ a
⊢ (1 - 1 / a)⁻¹ ≤ 2
refine' (inv_le_inv_of_le (inv_pos.2 <| zero_lt_two' α) _).trans_eq (inv_inv (2 : α))
ι : Type ?u.187185
α : Type u_1
β : Type ?u.187191
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
a2 : 2 ≤ a
⊢ 1 / a ≤ 1 - 2⁻¹
ι : Type ?u.187185
α : Type u_1
β : Type ?u.187191
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
a2 : 2 ≤ a
⊢ 2⁻¹ ≤ 1 - 1 / a
rw [le_sub_iff_add_le, add_comm, ←le_sub_iff_add_le]
case h.e'_4
ι : Type ?u.187185
α : Type u_1
β : Type ?u.187191
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
a2 : 2 ≤ a
⊢ 1 - 2⁻¹ = 2⁻¹
ι : Type ?u.187185
α : Type u_1
β : Type ?u.187191
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
a2 : 2 ≤ a
⊢ 1 / a ≤ 1 - 2⁻¹
convert (one_div a).le.trans (inv_le_inv_of_le zero_lt_two a2) using 1
no goals
case h.e'_4
ι : Type ?u.187185
α : Type u_1
β : Type ?u.187191
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
a2 : 2 ≤ a
⊢ 1 - 2⁻¹ = 2⁻¹
rw [sub_eq_iff_eq_add, ←two_mul, mul_inv_cancel two_ne_zero]