proposition: Theorem add_assoc: forall p1 p2 p3, add p1 (add p2 p3) = add (add p1 p2) p3.
proof: Proof. intros p1 p2 p3. case (ceqb p1 inf_elt); intros H1. apply degen_assoc; auto. case (ceqb p2 inf_elt); intros H2. apply degen_assoc; auto. case (ceqb p3 inf_elt); intros H3. apply degen_assoc; auto. case (ceqb p1 p2); intros H4. subst p1. rewrite add_comm; rewrite (add_comm p2). rewrite <- spec4_assoc; rewrite add_comm; auto. case (ceqb p1 (opp p2)); intros H5. apply degen_assoc; auto. case (ceqb p2 p3); intros H6. subst p2. apply spec4_assoc. case (ceqb p2 (opp p3)); intros H7. apply degen_assoc; auto. case (ceqb (opp p1) (add p2 p3)); intros H8. apply degen_assoc; auto. case (ceqb (opp p3) (add p1 p2)); intros H9. apply degen_assoc; auto. case (ceqb p1 (add p2 p3)); intros H10. rewrite H10. apply cancel with (opp p3). rewrite spec4_assoc. repeat rewrite (add_comm (opp p3)). repeat rewrite add_minus_id; rewrite add_comm; auto. case (ceqb p3 (add p1 p2)); intros H11. rewrite H11. apply cancel with (opp p1). rewrite spec4_assoc. repeat rewrite (add_comm (opp p1)). repeat rewrite (add_comm p1). repeat rewrite add_minus_id; rewrite add_comm; auto. apply spec1_assoc. split; auto. split; auto. split; auto. intros HH; case H5; apply uniq_opp; auto. rewrite add_comm; auto. repeat split; auto. intros HH; case H7; apply uniq_opp; auto. rewrite add_comm; auto. intros HH; case H8; rewrite HH; rewrite opp_opp; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith