proposition: Theorem pe2e_add p1 p2 : pe2e (padde p1 p2) = adde (pe2e p1) (pe2e p2).
proof: Proof. case: p1 => x1 y1 z1 e1; case: p2 => x2 y2 z2 e2. rewrite /padde /pe2e. case: wb => [] [] p; rewrite /= p //. case: wb => [] [] p1; rewrite /= p1. case: wb => [] [|p2]; first by rewrite p. by apply: curve_elt_irr. case: eqP => x1z1E. case: eqP => y1z1E. case: eqP => [x2z1E|[]]; last first. by rewrite -[x2](divfK (_ : z2 != 0)) ?p1 // -x1z1E mulrAC divfK ?p // subrr. case: eqP => y2z1E /=; last first. by case: wb => [] [] p2; have := p2; rewrite eqxx. case: wb => [] [] p2 //. suff : 2%:R * y1 * z2 == 0. rewrite !mulf_eq0 (negPf (K2D0 Eth)) p1 orbF /= => /eqP y1Z. by case/idP: p2; rewrite y1Z !(mul0r, mulr0). apply/eqP. apply: etrans (_ : - (y2 * z1 - y1 * z2) + (y2 * z1 + (y1 / z1 * z1 * z2)) = 0). by field; rewrite p. by rewrite y2z1E oppr0 y1z1E mulrAC !mulNr divfK ?p1 // subrr add0r. case: eqP => [x2z1E | []]; last first. by rewrite -[x2](divfK (_ : z2 != 0)) ?p1 // -x1z1E mulrAC divfK ?p // subrr. case: eqP => y2z1E. have y1NZ : y1 != 0. apply/eqP => y1Z; case: y1z1E. have/eqP := y2z1E . rewrite y1Z !mul0r subr0 mulf_eq0 p orbF => /eqP->. by rewrite mul0r oppr0. case: wb => [] [] p3. by move: (p3); rewrite !mulf_eq0 p (negPf (K2D0 Eth)) (negPf y1NZ). by apply: curve_elt_irr; field; rewrite p y1NZ (negPf (K2D0 Eth)). have: (y1 / z1) ^+ 2 == (y2 / z2) ^+ 2. apply/eqP. apply: etrans (_ : (y1 ^+ 2 * z1 / z1^+ 3 = _)); first by field; rewrite p. rewrite e1. apply: etrans (_ : (y2 ^+ 2 * z2 / z2^+ 3 = _)); last by field; rewrite p1. rewrite e2. have/eqP := x2z1E; rewrite subr_eq0 => /eqP He1. by field: He1; rewrite p p1. rewrite eqf_sqr. have /eqP/negPf-> := y1z1E. rewrite GRing.eqr_div ?p ?p1 // -subr_eq0 -opprB oppr_eq0. by have /eqP/negPf-> := y2z1E. case: eqP => [x2z1E|/eqP x2z1E]. case: x1z1E; apply/eqP. by rewrite GRing.eqr_div ?p ?p1 // eq_sym -subr_eq0 x2z1E. case: wb => [] [|p2]. by rewrite !mulf_eq0 p p1 (negPf x2z1E). by apply: curve_elt_irr; field; rewrite p p1 mulNr x2z1E. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)