case inl
R : Type u_1
inst✝ : LinearOrderedField R
x y : R
h : x ≤ y
⊢ x + x = x + y - (y - x)
R : Type u_1
inst✝ : LinearOrderedField R
x y : R
⊢ min x y = 2⁻¹ * (x + y - abs (x - y))
cases' le_total x y with h h <;> field_simp [h, abs_of_nonneg, abs_of_nonpos, mul_two]
no goals
case inl
R : Type u_1
inst✝ : LinearOrderedField R
x y : R
h : x ≤ y
⊢ x + x = x + y - (y - x)
abel