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: Jun 17 2024 at 22:01 UTC