proposition: Lemma add_zero: forall x1 x2 y1 y2, x1 = x2 -> y1 ^ 2 = x1 ^ 3 + A * x1 + B -> y2 ^ 2 = x2 ^ 3 + A * x2 + B -> y1 <> -y2 -> y1 = y2.
proof: Proof. intros x1 x2 y1 y2 H H1 H2 H3; subst x2. case (@Kmult_integral (y1 - y2) (y1 + y2)); try (intros H4; apply Keq_minus_eq; auto). ring [H1 H2]. case H3; apply Keq_minus_eq; rewrite <- H4; ring. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith