proposition: Theorem oppe_adde p1 p2 : oppe (adde p1 p2) = adde (oppe p1) (oppe p2).
proof: Proof. case: p1 => [|x1 y1 e1]; first by rewrite oppe0 !add0e. case p2 => [|x2 y2 e2/=]; first by rewrite !adde0. case: eqP => [x1Ex2|x1Dx2]; last first. by apply: curve_elt_irr; field; rewrite subr_eq0 eq_sym; apply/eqP. case: eqP => [y1ENy2|y1DNy2]. by case: eqP => [//|[]]; rewrite y1ENy2. case: eqP => [Ny1ENNy2|Ny1DNNy2]. by case: y1DNy2; rewrite -(opprK y1) Ny1ENNy2 opprK. have y1NZ : y1 != 0 by apply: adde_zero_diff x1Ex2 e1 e2 y1DNy2. by apply: curve_elt_irr; field; rewrite oppr_eq0 (negPf K2D0) y1NZ. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)