The prose says > Let x and y be real numbers and suppose that x=2 or y=-2. Show that x^2 + 2x = 2y + 4. But the code says ``` example {x y : ℝ} (h : x = 2 ∨ y = -2) : x * y + 2 * x = 2 * y + 4 := by sorry ``` The inconsistency is x*x vs x*y.
The prose says
But the code says
The inconsistency is xx vs xy.