proposition: Theorem add_comm: forall p1 p2, add p1 p2 = add p2 p1.
proof: Proof. intros p1 p2; case p1. rewrite add_0_r; rewrite add_0_l; auto. intros x1 y1 H1; case p2. rewrite add_0_r; rewrite add_0_l; auto. intros x2 y2 H2; simpl; repeat ksplit. case KD2; ring [KD0]. case KD0; ring [KD2]. assert (H3 := add_zero KD H1 H2 KD0). apply curve_elt_irr; subst x2 y2; auto. case KD; auto. case KD; auto. apply curve_elt_irr; field; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith