proposition: Theorem adde_casew 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 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) (p1DNp2 : p1 != oppe p2) (HC : [/\ x1 = x2, y1 = y2 & l = (3%:R * x1 ^+ 2 + A) / (2%:R * y1)] \/ (x1 != x2 /\ 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 Hg p q; apply: adde_case => //. move=> p1 x1 y1 e1 p2 x2 y2 e2 l p1E p2E p2E1 y1NZ lE x2E y2E. apply: (Hg p1 x1 y1 e1 p1 x1 y1 e1 p2 x2 y2 e2 l) => //. - apply/eqP; rewrite p1E /= => [] [y1E]. have /eqP : 2%:R * y1 = 0 by rewrite mulr_natl mulr2n {1}y1E; ring. by rewrite mulf_eq0 (negPf K2D0) (negPf y1NZ). - by left. by ring: x2E. move=> p1 x1 y1 e1 p2 x2 y2 e2 p3 x3 y3 e3 l p1E p2E p3E p3E1 x1Dx2 lE x3E y3E. apply: (Hg p1 x1 y1 e1 p2 x2 y2 e2 p3 x3 y3 e3 l) => //. apply/eqP; rewrite p1E p2E => [] [] x1Ex2. by case/eqP: x1Dx2. by right; split. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)