linarith Cannot Handle 2⁻¹

[yangky11]

Hi,

I just found that linarith can solve

x: ℝ
h₀: x * (1 / 2 + 2 / 3) = 1
⊢ x = 6 / 7

but cannot solve

x: ℝ
h₀: x * (2⁻¹ + 2 / 3) = 1
⊢ x = 6 / 7

Would it be possible/desirable for linarith to recognize that 2⁻¹ is also in the linear arithmetic fragment?

More context: This behavior has prevented aesop from proving some theorems (see leanprover-community/aesop#76). The second goal is the result of applying simp_all to the first goal, and simp_all is used extensively in aesop for normalizing proof goals.