proposition: Theorem aux1: forall x1 y1 x2 y2, y1 ^ 2 = x1 ^ 3 + A * x1 + B -> y2 ^ 2 = x2 ^ 3 + A * x2 + B -> x1 <> x2 -> y2 = 0 -> ((y2 - y1) / (x2 - x1))^2 - x1 - x2 = x2 -> False.
proof: Proof. intros x1 y1 x2 y2 H H1 H2 H3 H4. subst y2. assert (Hu : x2 ^ 3 = -(A * x2 + B)). apply trans_equal with ((x2 ^ 3 + A * x2 + B) - (A * x2 + B)); try ring. rewrite <- H1; ring. assert (H5:= (Keq_minus_eq_inv H4)); clear H4. field_simplify_eq [H Hu] in H5; auto. generalize (Kmult_eq_compat_l x2 H5); rename H5 into H4. replace (x2 * 0) with 0; try ring; intros H5. field_simplify_eq [Hu] in H5. generalize H5; clear H5. match goal with |- (?X = _ -> _) => replace X with ((x2 - x1) * (2* A *x2 + 3* B)); try ring end. intros tmp; case (Kmult_integral tmp); clear tmp; intros HH2. case H2; apply sym_equal; apply Keq_minus_eq; auto. generalize (Kmult_eq_compat_l ((2 * A )^3) (sym_equal H1)). replace ((2 * A)^3 * 0 ^ 2) with 0; try (ring). intros H5; ring_simplify in H5; auto. match type of H5 with (?X + ?Y + _ = _) => let x := (constr:(2 * A * x2)) in ((replace Y with (x ^ 3) in H5; try ring); (replace X with (4 * A^3 * x) in H5; try ring); replace x with (-(3) * B) in H5) end. 2: apply sym_equal; apply Keq_minus_eq; apply trans_equal with (2:= HH2); ring. ring_simplify in H5; auto. match type of Eth.(NonSingular) with ?X <> 0 => case (@Kmult_integral (-B) X); try intros HH3; try (case NonSingular; auto; fail) end. rewrite <- H5; ring. assert (HH3b : B = 0). replace B with (-(-B)); try ring; rewrite HH3; ring. case (@Kmult_integral 2 (A * x2)); try intros HH4; auto. apply trans_equal with (2:= HH2). rewrite HH3b; ring. case (Kmult_integral HH4); try intros HH5; auto. case Eth.(NonSingular); rewrite HH3b; rewrite HH5; simpl; ring. ring_simplify [HH5] in H4; auto. case (@Kmult_integral A x1); try intros HH6; auto. apply trans_equal with (2 := H4); rewrite HH3b; ring. case Eth.(NonSingular); rewrite HH3b; rewrite HH6; ring. case H2; rewrite HH6; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith