proposition: Lemma adde_zero x1 x2 y1 y2 : x1 = x2 -> y1 ^+ 2 = x1 ^+ 3 + A * x1 + B -> y2 ^+ 2 = x2 ^+ 3 + A * x2 + B -> y1 != - y2 -> y1 = y2.
proof: Proof. move=> x1E e1 e2 y1DNy2. have /eqP : (y1 - y2) * (y1 + y2) = 0 by ring: x1E e1 e2. rewrite mulf_eq0 => /orP[] /eqP Hy. by rewrite -[y1](subrK y2) Hy; ring. case/eqP: y1DNy2. by rewrite -[y1](addrK y2) Hy; ring. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)