proposition: Theorem addeK p1 p2 : adde (adde p1 p2) (oppe p2) = p1.
proof: Proof. have [p1Dp2ENp2 | /eqP] := adde p1 p2 =P oppe p2. rewrite p1Dp2ENp2; apply/sym_equal/adde_oppe_double_opp. by rewrite addeC. elim/adde_case: (adde p1 p2) => {p1 p2}// [p pDNp|p pDNp|p infDNNp||]. - by rewrite addeN. - by rewrite adde0. - by rewrite oppeK. - move=> p1 x1 y1 e1 p2 x2 y2 e2 l p1E p2E p2E1 y1NZ lE x2E y2E p2DNp1. rewrite p2E1. apply: compat_addeK => //. rewrite p1E /=; apply/eqP => [] [y1E]. suff: 2%:R * y1 == 0 by rewrite mulf_eq0 (negPf K2D0) (negPf y1NZ). by rewrite mulr_natl mulr2n [X in _ + X]y1E addrN. - by rewrite -p2E1. move=> p1 x1 y1 e1 p2 x2 y2 e2 p3 x3 y3 e3 l p1E p2E p3E p3E1 x1Dx2 lE x3E y3E. move: p2E p3E p3E1; rewrite -[in p2 = _](oppeK p2) -[in adde _ p2](oppeK p2). elim/adde_case: (adde p3 (oppe p2)) => {p3}// [p *||]. - apply/sym_equal/(uniq_zeroe (_ : _ = p)) => //. by rewrite -[in LHS](oppeK p). - by move=> ? ? ? ? ? ? ? ? ?; rewrite eqxx. move=> p4 x4 y4 e4 p5 x5 y5 e5 p6 x6 y6 e6 l0 -> -> -> _. move=> x4Dx5 l0E x6E y6E [x5E Ny5E] [x4E y4E] _ _. have y5E : y5 = - y2 by rewrite -Ny5E opprK. rewrite p1E. by apply: curve_elt_irr; rewrite ?y6E ?x6E ?l0E ?y5E ?y4E ?x5E ?x4E ?y3E ?x3E ?lE; field: e1 e2; rewrite subr_eq0 [in x2 != _]eq_sym ?x1Dx2 /=; apply/eqP => polE; case/eqP: x4Dx5; rewrite x4E x3E lE x5E; apply/eqP; rewrite -subr_eq0; apply/eqP; (rewrite (_ : 0 = 0 / -(x2 - x1) ^+ 2); last by rewrite mul0r); rewrite -polE; field: e1 e2; rewrite oppr_eq0 expf_eq0 /= subr_eq0 eq_sym (negPf x1Dx2). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)