proposition: Theorem adde_oppe_double_opp p1 p2 : adde p1 p2 = oppe p1 -> p2 = adde (oppe p1) (oppe p1).
proof: Proof. move=> p1Dp2E. have [p1ENp1 | /eqP p1DNp1] := (p1 =P oppe p1). rewrite -[X in adde X]p1ENp1 addeN. apply: uniq_zeroe (_ : _ = p1). by rewrite addeC p1Dp2E. rewrite -oppe_adde. suff [] : p2 = adde (oppe p1) (oppe p1) \/ p2 = oppe (adde (oppe p1) (oppe p1)). - by rewrite <- oppe_adde. - rewrite oppe_adde !oppeK => p2E. have [p1Dp1E|/eqP p1Dp1DNp1] := adde p1 p1 =P oppe p1. by rewrite p2E p1Dp1E -p1Dp2E p2E p1Dp1E addeN. rewrite -p2E. apply: addeI_oppe (_ : _ != oppe p1) => //. apply: etrans (_ : oppe (adde (adde p1 p1) (oppe p1)) = _). by rewrite compat_addeK //. by rewrite -p2E oppe_adde oppeK addeC. rewrite -oppe_adde oppeK. elim/adde_case: (adde p1 p2) p1Dp2E p1DNp1 => {p1 p2}// [p pE /eqP[]//| p pE _||]. - by rewrite oppe_adde -pE; left. - move=> p1 x1 y1 e1 p2 x2 y2 e2 l p1E p2E p2E1 p1NZ lE x2E y2E p2E2 p1DNp1. by rewrite -p2E1 p2E2 oppeK; left. move=> p1 x1 y1 e1 p2 x2 y2 e2 p3 x3 y3 e3 l p1E p2E p3E p3E1 x1Dx2 lE x3E y3E p3E2 p1DNp1. have [y1Z | /eqP y1NZ] := y1 =P 0. by case/eqP: p1DNp1; rewrite p1E; apply: curve_elt_irr; rewrite ?y1Z ?oppr0. have Ny1NZ : - y1 != 0 by rewrite oppr_eq0. have := p3E2. rewrite p1E p2E p3E /=. case: eqP => [x1Ex1 | //]. case: eqP => [/eqP | y1DNy1]. by rewrite -subr_eq0 opprK -mulr2n -mulr_natl mulf_eq0 (negPf K2D0) (negPf y1NZ). case => x3E1 y3E1; subst x3 y3. have : forall P Q, P \/ Q -> Q \/ P by move=> P Q []; [right|left]. apply; apply: curve_elt_oppe. move/eqP: x3E1; rewrite lE -subr_eq0 => /eqP polE. suff : (x2 - (((3%:R * x1 ^+ 2 + A) / (2%:R * y1))^+ 2 - 2%:R * x1)) * (x2 - x1) ^+ 2 == 0. rewrite mulf_eq0 expf_eq0 /= !subr_eq0 [_ == x1]eq_sym (negPf x1Dx2) orbF. by move/eqP. apply/eqP. suff pol1E : (2%:R * y2 * y1) ^+ 2 - (x2 * A + 3%:R * x2 * x1 ^ 2 + A * x1 - x1 ^+ 3 + 2%:R * B) ^+ 2 = 0. rewrite (_ : 0 = 0 / (2%:R * y1) ^+ 2); last first. by rewrite mul0r. rewrite -pol1E. by field: e1 e2; rewrite y1NZ K2D0. apply/eqP; rewrite subr_eq0; apply/eqP. congr (_ ^+ _). apply/eqP; rewrite -subr_eq0; apply/eqP. rewrite (_ : 0 = 0 * -(x2 - x1) ^+ 2); last by rewrite mul0r. rewrite -polE. by field: e1 e2; rewrite subr_eq0 eq_sym. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)