proposition: Theorem cancel: forall p1 p2 p3, add p1 p2 = add p1 p3 -> p2 = p3.
proof: Proof. intros p1 p2; pattern p1, p2, (add p1 p2); apply add_casew; clear p1 p2. intros; subst; auto. intros p p1 H; symmetry; apply uniq_zero with p. rewrite add_comm; auto. intros; symmetry; apply uniq_opp; auto. intros p1 x1 y1 H1 p2 x2 y2 H2 p4 x4 y4 H4 l Hp1 Hp2 Hp4 Hp4b Hd1 Hl1 Hx4 Hy4 p3. generalize Hp1 Hp4b Hd1; clear Hp1 Hp4b Hd1. rewrite Hp4; clear Hp4. pattern p1, p3, (add p1 p3); apply add_casew; clear p1 p3. intros; discriminate. intros p He1 He2 _ He3. apply uniq_zero with p. rewrite add_comm; rewrite <- He2; auto. intros; discriminate. intros p1 x1b y1b H1b p3 x3 y3 H3 p5 x5 y5 H5 l'. intros Hp1b Hp3 Hp5 Hp5b Hd1 Hl' Hx5 Hy5 He1 He2 Hd2 He3. rewrite He3 in He2; rewrite Hp5b in He2. rewrite He1 in Hp1b; injection Hp1b; clear Hp1b. intros; subst x1b y1b. generalize He3; rewrite Hp5. intros tmp; injection tmp; intros HH HH1; clear tmp. rewrite Hp5b in He3. generalize Hy5; clear Hy5. rewrite <- HH; rewrite <- HH1; rewrite Hy4; clear HH Hy4. intros HH2; generalize (Keq_minus_eq_inv HH2); clear HH2. intros HH2; ring_simplify in HH2. case (@Kmult_integral (l' - l) (x4 - x1)); try (clear HH2; intros HH2). rewrite <- HH2; ring. generalize HH1; subst x4 x5; clear HH1. rewrite (Keq_minus_eq HH2). intros HH; generalize (Keq_minus_eq_inv HH); clear HH; intros HH; ring_simplify in HH. case (curve_elt_opp H2 H3). symmetry; apply Keq_minus_eq; rewrite <- HH; ring. subst p2 p3; auto. rewrite <- Hp2; rewrite <- Hp3; intros HH1. case (ceqb p1 (opp p1)); intros HH3. case Hl1; clear Hl1. intros (Hx1, (Hy1, _)). case Hd1; rewrite <- HH1; rewrite He1; rewrite Hp2; apply curve_elt_irr; auto; clear Hd1. intros (Hdx1, Hl2); rewrite Hl2 in HH2; clear Hl2. case Hl'; clear Hl'. intros (Hx1, (Hy1, _)). case Hd2; rewrite HH1; rewrite opp_opp. rewrite He1; rewrite Hp3; apply curve_elt_irr; auto; clear Hd1. intros (Hdx3, Hl2); rewrite Hl2 in HH2; clear Hl2. generalize HH1; rewrite Hp2; rewrite Hp3; simpl; clear HH1. intros tmp; injection tmp. intros; apply curve_elt_irr; auto. subst x3 y2. field_simplify_eq in HH2; auto. case (Kmult_integral HH2); try intros HHx; auto. case Kdiff_2_0; auto. ring [HHx]. rewrite <- (opp_opp p3); rewrite <- HH1. apply compat_add_opp with p1; auto. pattern p2 at 2; rewrite HH1; rewrite opp_opp; auto. case (curve_elt_opp H4 H1); try apply Keq_minus_eq; auto; rewrite He3; rewrite <- He1; intros HH3. apply trans_equal with inf_elt; [idtac | symmetry]; apply uniq_zero with p1; rewrite add_comm; auto. rewrite <- He2; auto. apply trans_equal with (add (opp p1) (opp p1)); [idtac | symmetry]; apply add_opp_double_opp; auto. rewrite <- He2; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith