proposition: Theorem addeC p1 p2 : adde p1 p2 = adde p2 p1.
proof: Proof. case: p1 => /= [|x1 y1 e1]; first by rewrite adde0. case: p2 => //= x2 y2 e2. case: eqP => [x1Ex2 | x1Dx2]. case: eqP => [y1ENy2|y1DNy2]. case: eqP => [x1E1x2| []//]. by case: eqP => // [] []; rewrite y1ENy2 opprK. case: eqP => [x2Ex1 | []//]. case: eqP => [y2ENy1|y2DNy1]; first by case: y1DNy2; rewrite y2ENy1 opprK. by apply curve_elt_irr; rewrite x1Ex2 (adde_zero _ e1 e2) //; apply/eqP. case: eqP => [x2Ex1|x2Dx1]; first by case: x1Dx2. by apply curve_elt_irr; field; rewrite !subr_eq0; have /eqP-> := x1Dx2; have /eqP-> := x2Dx1. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)