proposition: Theorem add_minus_id: forall p1 p2, (add (add p1 p2) (opp p2)) = p1.
proof: Proof. intros p1 p2. case (ceqb (add p1 p2) (opp p2)). intros Hp12; rewrite Hp12; symmetry; apply add_opp_double_opp; rewrite add_comm; auto. pattern p1, p2, (add p1 p2); apply add_case; clear p1 p2. intros; rewrite add_opp; auto. intros; rewrite add_0_r; auto. intros; rewrite opp_opp; auto. intros p1 x1 y1 H1 p2 x2 y2 H2 l Hp1 Hp2 Hp3 Hd Hl Hx2 Hy2 Hp12. rewrite Hp3. apply compat_add_triple; auto. rewrite Hp1; simpl; intros tmp; case Hd; injection tmp; intros; apply Keq_opp_is_zero; auto. rewrite <- Hp3; auto. intros p1 x1 y1 H1 p2 x2 y2 H2 p3 x3 y3 H3 l Hp1 Hp2 Hp3 Hp3b Hx1 Hl Hx3 Hy3. generalize Hp2 Hp3 Hp3b; clear Hp2 Hp3 Hp3b. pattern p2 at 1 2; rewrite <- (opp_opp p2). pattern p3, (opp p2), (add p3 (opp p2)). apply add_case. intros; discriminate. intros; discriminate. intros; symmetry; apply uniq_zero with p. pattern p at 1; rewrite <- (opp_opp p); auto. intros; case n; auto. intros p4 x4 y4 H4 p5 x5 y5 H5 p6 x6 y6 H6 l0. intros Hp4; rewrite Hp4; clear Hp4. intros Hp5; rewrite Hp5; clear Hp5. intros Hp6 _; rewrite Hp6; clear Hp6. intros Hx Hl0 Hx6 Hy6. intros tmp; injection tmp; intros HH1 HH2; clear tmp. assert (y5 = - y2). rewrite <- HH1; ring. subst y5 x5; clear HH1. intros tmp; injection tmp; intros HH1 HH2; subst y4 x4; clear tmp. intros _ _. subst p1; apply curve_elt_irr; clear H6 H5 H4 H3; subst; apply Keq_minus_eq; field [H1 H2]; split; auto; intros HH; case Hx; ring_simplify [H1 H2] in HH; symmetry; apply Keq_minus_eq; field_simplify_eq [H1 H2]; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith