fact: Definition adde (p1 p2 : elt) : elt := if p1 is curve_elt x1 y1 e1 then if p2 is curve_elt x2 y2 e2 then match x1 =P x2 with | ReflectT x1Ex2 => match y1 =P - y2 with | ReflectT _ => inf_elt | ReflectF y1DNy2 => let l := (3%:R * x1 ^+ 2 + A) / (2%:R * y1) in let x3 := l ^+ 2 - 2%:R * x1 in @curve_elt x3 (-y1 - l * (x3 - x1)) (adde_lem1 (adde_zero_diff x1Ex2 e1 e2 y1DNy2) e1) end | ReflectF x1Dx2 => let l := (y2 - y1) / (x2 - x1) in let x3 := l ^+ 2 - x1 -x2 in @curve_elt x3 (- y1 - l * (x3 - x1)) (adde_lem2 x1Dx2 e1 e2) end else p1 else p2.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)