WKroneman (Aug 30 2020 at 16:01): WKroneman (Aug 30 2020 at 16:01):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
WKroneman (Aug 30 2020 at 16:17):Or is there a way to re-order the terms to make them match the other sum?
WKroneman (Aug 30 2020 at 16:51):Never mind, ring_simplify on goal and hypothesis separately works fine.
Last updated: Oct 08 2024 at 15:02 UTC