Ok, this would seem fairly trivial... Is there an easy tactic to solve this one?
H : s1x² - c1x² * e0² + c1x² - e0² * c1y² - 2 * s1x * c1x + s1y² + c1y² - 2 * s1y * c1y = 0
s1x² - e0² * c1x² - e0² * c1y² + c1x² - 2 * s1x * c1x + s1y² + c1y² - 2 * s1y * c1y = 0
Or is there a way to re-order the terms to make them match the other sum?
Never mind, ring_simplify on goal and hypothesis separately works fine.
Last updated: Sep 30 2023 at 06:01 UTC