proposition: Lemma add_lem1: forall x1 y1, y1 <> 0 -> y1 ^ 2 = x1 ^ 3 + A * x1 + B -> let l := (3 * x1 * x1 + A) / (2 * y1) in let x3 := l ^ 2 - 2 * x1 in (- y1 - l * (x3 - x1)) ^ 2 = x3 ^ 3 + A * x3 + B.
proof: Proof. intros x1 y1 H H1 l x3; unfold x3, l. Time field [H1]. split; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith