proposition: Lemma adde_lem2 x1 y1 x2 y2 : x1 <> x2 -> y1 ^ 2 = x1 ^ 3 + A * x1 + B -> y2 ^ 2 = x2 ^ 3 + A * x2 + B -> let l := (y2 - y1) / (x2 - x1) in let x3 := l ^ 2 - x1 - x2 in (- y1 - l * (x3 - x1)) ^ 2 = x3 ^ 3 + A * x3 + B.
proof: Proof. move=> /eqP x1Dx2 y1E y2E l x3; rewrite /x3 /l. Time field: y1E y2E. apply: contra_neq x1Dx2 => x2Bx1. by rewrite -[x2](subrK x1) x2Bx1; ring. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)