proposition: Theorem curve_elt_opp: forall x1 x2 y1 y2 H1 H2, x1 = x2 -> @curve_elt x1 y1 H1 = @curve_elt x2 y2 H2 \/ @curve_elt x1 y1 H1 = opp (@curve_elt x2 y2 H2).
proof: Proof. intros x1 x2 y1 y2 H1 H2 H3. case (@Kmult_integral (y1 - y2) (y1 + y2)); try intros H4. ring_simplify. ring [H1 H2 H3]. left; apply curve_elt_irr; auto. apply Keq_minus_eq; auto. right; unfold opp; apply curve_elt_irr; auto. apply Keq_minus_eq; rewrite <- H4; ring. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith