rw [hx2x2]
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
hx2x2 : x / 2 + x / 2 = 2 * x / 2
⊢ x / 2 + x / 2 = x
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
hx2x2 : x / 2 + x / 2 = 2 * x / 2
⊢ 2 * x / 2 = x