proposition: Theorem compat_addeK p : p != oppe p -> adde p p != oppe p -> adde (adde p p) (oppe p) = p.
proof: Proof. set p1 := adde p p; set p2 := oppe p. have : p1 = adde p p by []; have : p2 = oppe p by []. elim/adde_case: (adde p1 p2) => {p1 p2}// [p1 -> inE pDNp infDNp| p1 Np1ENp _ /eqP[]| p1 Np1ENp p1E pDNp1 p1DNp1||]. - by apply/sym_equal/uniq_oppe. - by rewrite -(oppeK p) -Np1ENp. - have pE : p = p1 by rewrite -(oppeK p) -Np1ENp oppeK. - apply/sym_equal/(uniq_zeroe (_ : _ = p)). by rewrite [RHS]pE. - by move=> p1 x1 y1 e1 p2 x2 y2 e2 l _ _ _ _ _ _ _ _ _ _ /eqP[]. move=> p1 x1 y1 e1 p2 x2 y2 e2 p3 x3 y3 e3 l p1E p2E p3E p3E1 x1Dx2 lE x3E y3E p2E1 p1E1 pDp2 p1Dp2. case: p p2E1 p1E1 pDp2 => [-> //|x y e p2E1 p1E1 eE]. move: (p2E1); rewrite p2E => [] [x2E y2E]. subst x2 y2; rewrite p3E. have [] // := curve_elt_oppe e3 e; last first. rewrite -p3E => p3E2. have /eqP[] : p1 != inf_elt by rewrite p1E. apply: (uniq_zeroe (_ : _ = p2)). by rewrite -p3E1 p2E1. rewrite x3E lE; move: p1E1 => /=. case: eqP => // xEx. case: eqP => [_|yDNy]; first by rewrite p1E => /eqP. rewrite p1E => [] [x1E y1E]; subst x1 y1. set l1 := (3%:R * x ^+2 + A) / (2%:R * y). by field; rewrite subr_eq0 eq_sym. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)