proposition: Theorem compat_add_triple: forall p, p <> opp p -> add p p <> opp p -> add (add p p) (opp p) = p.
proof: Proof. intro p. set (p1 := (add p p)). set (p2 := opp p). cut (p1 = add p p); auto. cut (p2 = opp p); auto. kcase p1 p2. intros p1 Hp1; subst p1. intros; symmetry; apply uniq_opp; auto. intros p1 H1 _ H2 _; case H2. rewrite <- (opp_opp p); rewrite <- H1; auto. intros p1 H1 H2 H3 H4. assert (H5: p = p1). rewrite <- (opp_opp p); rewrite <- H1; rewrite opp_opp; auto. subst p1. symmetry; apply uniq_zero with p; auto. intros; case H11; auto. case p; clear p. intros; subst p2; discriminate. intros x y H. set (p := (@curve_elt x y H)). intros p1 x1 y1 H1 p2 x2 y2 H2 p3 x3 y3 H3 l Hp1 Hp2 Hp3 Hp3b Hx12 Hl Hx3 Hy3 He1 He2 He3 He4. generalize He1; unfold p; rewrite Hp2; simpl; intros tmp; injection tmp; clear tmp. intros; subst x2 y2. rewrite Hp3. case (curve_elt_opp H3 H); auto. rewrite Hx3; rewrite Hl. generalize He2; unfold p; simpl; repeat ksplit. rewrite Hp1; intros; discriminate. rewrite Hp1; intros tmp; injection tmp; intros; subst x1 y1. set (l1 := (3 * x * x + A) / (2 * y)). field; repeat split; auto. rewrite <- Hp3; fold p; intros HH. absurd (p1 = inf_elt). rewrite Hp1; intros; discriminate. apply uniq_zero with p2. rewrite <- Hp3b; rewrite He1; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith