proposition: Theorem opp_add: forall p1 p2, opp (add p1 p2) = add (opp p1) (opp p2).
proof: Proof. intros p1 p2; case p1. rewrite opp_0; repeat rewrite add_0_l; auto. intros x1 y1 H1; case p2. rewrite opp_0; repeat rewrite add_0_r; auto. intros x2 y2 H2; simpl; repeat ksplit; simpl. case KD1; ring [KD0]. case KD0; apply trans_equal with (-(-y1)); try ring; rewrite KD1; ring. assert (HH:= add_zero_diff KD H1 H2 KD0). apply curve_elt_irr; try field; repeat split; auto; intros HH1; case HH; symmetry; apply Keq_minus_eq; ring_simplify; auto. apply curve_elt_irr; try field; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith