proposition: Theorem adde_case P : (forall p, P inf_elt p p) -> (forall p, P p inf_elt p) -> (forall p, P p (oppe p) inf_elt) -> (forall p1 x1 y1 e1 p2 x2 y2 e2 l (p1E : p1 = (@curve_elt x1 y1 e1)) (p2E : p2 = (@curve_elt x2 y2 e2)) (p2E1 : p2 = adde p1 p1) (y1NZ : y1 != 0) (lE : l = (3 %:R* x1 ^+2 + A) / (2%:R * y1)) (x2E : x2 = l ^+ 2 - 2%:R * x1) (y2E : y2 = - y1 - l * (x2 - x1)), P p1 p1 p2) -> (forall p1 x1 y1 e1 p2 x2 y2 e2 p3 x3 y3 e3 l (p1E : p1 = (@curve_elt x1 y1 e1)) (p2E : p2 = (@curve_elt x2 y2 e2)) (p3E : p3 = (@curve_elt x3 y3 e3)) (p3E1 : p3 = adde p1 p2) (x1Dx2 : x1 != x2) (lE : l = (y2 - y1) / (x2 - x1)) (x3E : x3 = l ^+ 2 - x1 - x2) (y3E : y3 = -y1 - l * (x3 - x1)), P p1 p2 p3)-> forall p q, P p q (adde p q).
proof: Proof. move=> Hip Hpi HpNp Ht Hg [|x1 y1 e1] [|x2 y2 e2] //. rewrite /adde. case: (x1 =P x2) => [x1Ex2 | x1Ex2]. case: (y1 =P - y2) => [y1Ey2 | y1Ey2]. have ->// : curve_elt e2 = oppe (curve_elt e1). by apply: curve_elt_irr => //; ring: y1Ey2. have y1NZ : y1 != 0 by apply: adde_zero_diff e1 e2 _. have -> : curve_elt e2 = curve_elt e1. apply: curve_elt_irr; apply/sym_equal => //. by apply: adde_zero e1 e2 _ => //; apply/eqP. pose e3 := adde_lem1 (adde_zero_diff x1Ex2 e1 e2 y1Ey2) e1. apply: (Ht (curve_elt e1) x1 y1 e1 (curve_elt e3) _ _ e3) => //. rewrite /adde; (do 2 case: eqP => //) => y1E x1E; last first. by apply: curve_elt_irr. have /eqP : 2%:R * y1 = 0 by rewrite mulr_natl mulr2n {1}y1E; ring. by rewrite mulf_eq0 (negPf K2D0) (negPf y1NZ). pose e3 := adde_lem2 x1Ex2 e1 e2. apply: (Hg (curve_elt e1) x1 y1 e1 (curve_elt e2) x2 y2 e2 (curve_elt e3) _ _ e3) => //; last by apply/eqP. rewrite /adde; case: eqP => // x1Dx2. by apply: curve_elt_irr. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)