proposition: Theorem addeI_oppe p1 p2 : adde p1 p2 = adde p1 (oppe p2) -> p1 != oppe p1 -> p2 = oppe p2.
proof: Proof. elim/adde_case: (adde p1 p2) => {p1 p2}// [p infE /eqP[]||]. - by apply: uniq_oppe; rewrite -[X in adde _ X]oppeK. - intros p1 x1 y1 e1 p2 x2 y2 e2 l p1E p2E p2E1 y1NZ lE x2E y2E p2E2 p1ENp1. by apply uniq_oppe; rewrite -p2E1 p2E2 addeN. move=> p1 x1 y1 e1 p2 x2 y2 e2 p3 x3 y3 e3 l p1E p2E p3E p3E1 x1Dx2 lE x3E y3E p3E2 p1DN1. move: p3E2; rewrite p1E p2E p3E /=. case: eqP => [x1Ex2 //|x1Dx21 [/eqP]]; first by case/eqP: x1Dx2. rewrite x3E lE -subr_eq0 => /eqP polE _. have : - 4%:R * y2 * y1 == 0. apply/eqP; rewrite (_ : 0 = 0 * (x2 - x1) ^+ 2); last by rewrite mul0r. by rewrite -polE; field; rewrite subr_eq0 eq_sym. rewrite (natrM _ 2 2) !(mulf_eq0, oppr_eq0) (negPf K2D0) /=. case/orP=> [/eqP y2Z| /eqP y1Z]. by apply: curve_elt_irr; rewrite ?y2Z ?oppr0. by case/eqP: p1DN1; rewrite p1E; apply: curve_elt_irr; rewrite ?y1Z ?oppr0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)