proposition: Theorem add_opp_double_opp: forall p1 p2, add p1 p2 = opp p1 -> p2 = add (opp p1) (opp p1).
proof: Proof. intros p1 p2; intros H1. case (ceqb p1 (opp p1)); intros H2. pattern (opp p1) at 1; rewrite <- H2. rewrite add_opp; apply uniq_zero with p1. rewrite add_comm; rewrite H1; auto. rewrite <-opp_add. assert (H: (p2 = add (opp p1) (opp p1)) \/ (p2 = opp (add (opp p1) (opp p1)))). rewrite <- opp_add; rewrite opp_opp. generalize H1 H2; clear H1 H2; kcase p1 p2. intros p H2 H1; case H1; auto. intros p H2 H1; rewrite opp_add; rewrite <- H2; auto. intros p1 x1 y1 H1 p2 x2 y2 H2 l Hp1 Hp2 Hp2b Hy1 _ _ _ He1 He2. rewrite <- Hp2b; rewrite He1; rewrite opp_opp; auto. intros p1 x1 y1 H1 p2 x2 y2 H2 p3 x3 y3 H3 l Hp1 Hp2 Hp3 Hp3b Hx12 Hl Hx3 Hy3 He1 He2. assert (Hy1: y1 <> 0). intros HH; case He2; rewrite Hp1; simpl; apply curve_elt_irr; ring[HH]. assert (Hy2: -y1 <> 0). intros Hy2; case Hy1; apply trans_equal with (-(-y1)); try ring; rewrite Hy2; ring. generalize He1; clear He1. rewrite Hp1; rewrite Hp2; rewrite Hp3; simpl; repeat ksplit. case Hy1; apply Keq_opp_is_zero; auto. intros tmp; injection tmp; intros; subst x3 y3; clear tmp Hp1 Hp2 Hp3. assert (tmp: forall P Q, P \/ Q -> Q \/ P). intuition. apply tmp; apply curve_elt_opp; clear tmp. rewrite Hl in H0. assert (HH1:= (Keq_minus_eq_inv H0)); clear H0. field_simplify_eq [H1 H2] in HH1; auto. match type of HH1 with ?XX = 0 => assert (HH2: 2 * y2 * y1 = XX + 2 * y2 * y1); try (rewrite HH1; ring); clear HH1; rename HH2 into HH1; ring_simplify in HH1 end. match type of HH1 with _ = ?X => assert (HH2: 4 * y2^2 * y1^2 = X * X); [rewrite <- HH1;ring | clear HH1; rename HH2 into HH1] end. assert (HH2:= Keq_minus_eq_inv HH1); clear HH1; rename HH2 into HH1. ring_simplify [H1 H2] in HH1. assert (HH2: (x2 - (((3 * x1* x1 + A)/(2*-y1))^2 -2 * x1)) * (x2 -x1)^2 = 0). field_simplify_eq [H1]; auto. apply trans_equal with (2 := HH1); ring. clear HH1; rename HH2 into HH1. case (Kmult_integral HH1); intros HH2. apply Keq_minus_eq; auto. rewrite <- HH2; field; auto; split; auto. simpl in HH2; auto. case (Kmult_integral HH2); intros; case Hx12; symmetry; apply Keq_minus_eq; auto. case H; auto; intros H3. rewrite <- opp_add in H3; auto. rewrite opp_add in H3; rewrite opp_opp in H3. case (ceqb (add p1 p1) (opp p1)); intros H4. rewrite H3; rewrite H4. rewrite <- H1; rewrite H3; rewrite H4. rewrite add_opp; auto. rewrite <- H3. apply compat_add_opp with p1; auto. apply trans_equal with (opp(add (add p1 p1) (opp p1))). rewrite compat_add_triple; auto. rewrite <- H3; rewrite opp_add; rewrite opp_opp. apply add_comm. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith