proposition: Theorem adde_aux1 x1 y1 x2 y2 : y1 ^+ 2 = x1 ^+ 3 + A * x1 + B -> y2 ^+ 2 = x2 ^+ 3 + A * x2 + B -> x1 != x2 -> y2 = 0 -> ((y2 - y1) / (x2 - x1)) ^+ 2 - x1 - x2 != x2.
proof: Proof. move=> e1 e2 x1Dx2 y2Z; rewrite -subr_eq0; apply/eqP=> polE. have x23E : x2 ^+ 3 = -(A * x2 + B). by apply/eqP; rewrite -subr_eq0 opprK addrA -e2 y2Z expf_eq0 eqxx. have : (x2 - x1) * (2%:R * A * x2 + 3%:R * B) == 0 . rewrite (_ : 0 = 0 * (((x2 - x1) ^+ 2) * x2)); last by rewrite mul0r. rewrite -polE; apply/eqP. by field: y2Z e1 x23E; rewrite subr_eq0 eq_sym. rewrite mulf_eq0 subr_eq0 eq_sym (negPf x1Dx2) /= addr_eq0 => /eqP Ax2E. have BZ : B = 0. rewrite -[LHS]opprK. have : - B * (4%:R * A ^+ 3 + 27%:R * B ^+ 2) == 0. apply/eqP. have : (2%:R * A * x2) ^+ 3 + 4%:R * A ^+ 3 * (2%:R * A * x2) + 8%:R * A ^+ 3 * B = 8%:R * A ^+ 3 * y2 ^+ 2. by rewrite e2; ring. by rewrite y2Z expr0n mulr0 Ax2E => <-; ring. rewrite mulf_eq0 (negPf (NonSingular Eth)) orbF => /eqP->. by rewrite oppr0. have : 2%:R * A * x2 == 0 by rewrite Ax2E BZ mulr0 oppr0. rewrite !mulf_eq0 (negPf K2D0) /= => /orP[/eqP AZ|/eqP x2Z]. by case/eqP: (NonSingular Eth); rewrite AZ BZ !expr0n !mulr0 addr0. have : A * x1 == 0. apply/eqP; rewrite (_ : 0 = 0 * (x2 - x1) ^+ 2); last by rewrite mul0r. rewrite -polE y2Z x2Z !subr0 !sub0r. by field: e1 BZ; rewrite oppr_eq0 -x2Z. rewrite !mulf_eq0 => /orP[/eqP AZ|/eqP x1Z]. by case/eqP: (NonSingular Eth); rewrite AZ BZ !expr0n !mulr0 addr0. by case/eqP: x1Dx2; rewrite x2Z. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)