proposition: Theorem compat_add_opp: forall p1 p2, add p1 p2 = add p1 (opp p2) -> ~ p1 = opp p1 -> p2 = opp p2.
proof: Proof. intros p1 p2; kcase p1 p2. intros p H H1; case H1. apply uniq_opp. pattern p at 2; rewrite <- opp_opp; auto. intros p1 x1 y1 H1 p2 x2 y2 H2 l Hp1 Hp2 Hp2b Hy Hl Hx2 Hy2 He1 He2. apply uniq_opp. rewrite <- Hp2b; rewrite He1; rewrite add_opp; auto. intros p1 x1 y1 H1 p2 x2 y2 H2 p3 x3 y3 H3 l Hp1 Hp2 Hp3 Hp3b Hx12 Hl Hx3 Hy3 Hp3bb Hd. generalize Hp3bb; clear Hp3bb. subst p1 p2 p3; simpl; repeat ksplit. intros tmp; injection tmp; clear tmp. rewrite Hx3; rewrite Hl; intros _ HH. assert (HH1:= (Keq_minus_eq_inv HH)). field_simplify_eq in HH1; auto. case (Kmult_integral HH1); try intros HH2; auto. case (Kmult_integral HH2); try intros HH3; auto. assert (HH8: 2 * 2 = 0). replace (2*2) with (-(-(2 * 2))); try ring ; try rewrite HH3; ring. case (Kmult_integral HH8); try intro H9; case Kdiff_2_0; auto. intros; apply curve_elt_irr; try rewrite HH3; intros; ring. case Hd; simpl; apply curve_elt_irr; ring[HH2]. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith