Stream: Coq users

Topic: simplification of polynomial expressions


view this post on Zulip 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

view this post on Zulip WKroneman (Aug 30 2020 at 16:17):

Or is there a way to re-order the terms to make them match the other sum?

view this post on Zulip WKroneman (Aug 30 2020 at 16:51):

Never mind, ring_simplify on goal and hypothesis separately works fine.


Last updated: Jan 31 2023 at 13:02 UTC