proposition: Theorem curve_elt_oppe x1 x2 y1 y2 e1 e2 (x1E : x1 = x2) : @curve_elt x1 y1 e1 = @curve_elt x2 y2 e2 \/ @curve_elt x1 y1 e1 = oppe (@curve_elt x2 y2 e2).
proof: Proof. have /eqP : (y1 - y2) * (y1 + y2) = 0. ring: x1E e1 e2. rewrite mulf_eq0 => /orP[] /eqP Hy. left; apply: curve_elt_irr => //. by rewrite -[y1](subrK y2) Hy; ring. right. apply: curve_elt_irr => //. by rewrite -[y1](addrK y2) Hy; ring. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)