proposition: Lemma add_lem2: forall 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. intros x1 y1 x2 y2 H H1 H2 l x3; unfold x3, l. Time field [H1 H2]; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith