proposition: Theorem pe2e_double p1 : pe2e (pdouble p1) = adde (pe2e p1) (pe2e p1).
proof: Proof. case: p1 => x1 y1 z1 e1. rewrite /pdouble /pe2e. case: wb => [] [] p; rewrite p. case: wb => [] [] p1 //=. by case/idP : p1; rewrite p. have [y1Z|/eqP y1NZ] := y1 =P 0. case: wb => [] [] p1; last first. by case/idP: p1; rewrite y1Z !(mul0r, mulr0). rewrite /adde. case: eqP => [x1z1E| [//]]. case: eqP => [|[]] => //. by rewrite y1Z mul0r oppr0. case: wb => [] [] p1. move: (p1). by rewrite !mulf_eq0 p (negPf y1NZ) (negPf (K2D0 Eth)). rewrite /adde. case: eqP => [x1z1E| [//]]. case: eqP => y1z1E. have: (2%:R * (y1 / z1) == 0). by rewrite mulr_natl mulr2n [X in _ + X == _]y1z1E addrN. by rewrite !mulf_eq0 invr_eq0 p (negPf y1NZ) (negPf (K2D0 Eth)). by apply: curve_elt_irr => /=; field; rewrite y1NZ p (K2D0 Eth). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)