proposition: Lemma adde_zero_diff x1 x2 y1 y2 : x1 = x2 -> y1 ^+ 2 = x1 ^+ 3 + A * x1 + B -> y2 ^+ 2 = x2 ^+ 3 + A * x2 + B -> y1 <> - y2 -> y1 != 0.
proof: Proof. move=> x1E e1 e2 /eqP y1DNy2. have y1E := adde_zero x1E e1 e2 y1DNy2. apply: contra_neq y1DNy2. by rewrite -y1E => y2E; ring : y2E. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)