proposition: Lemma adde_lem1 x1 y1 : y1 != 0 -> y1 ^+ 2 = x1 ^+ 3 + A * x1 + B -> let l := (3%:R * x1 ^+2 + A) / (2%:R * y1) in let x3 := l ^+ 2 - 2%:R * x1 in (- y1 - l * (x3 - x1)) ^+ 2 = x3 ^+ 3 + A * x3 + B.
proof: Proof. move=> y1D0 y1E l x3; rewrite /x3 /l; field : y1E. by rewrite y1D0 K2D0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)