proposition: Theorem spec4_assoc: forall p1 p2, add p1 (add p2 p2) = add (add p1 p2) p2.
proof: Proof. intros p1 p2. case (ceqb p1 inf_elt); intros H1. apply degen_assoc; auto. case (ceqb p2 inf_elt); intros H2. apply degen_assoc; auto. case (ceqb p2 (opp p2)); intros H3. apply degen_assoc; auto. case (ceqb p1 (opp p2)); intros H4. apply degen_assoc; auto. case (ceqb (opp p1) (add p2 p2)); intros H5. apply degen_assoc; auto. case (ceqb (opp p2) (add p1 p2)); intros H6. apply degen_assoc; auto. case (ceqb p1 (add p2 p2)); intros H7. subst p1; apply spec3_assoc. repeat split; auto. intros H7; case H2; apply uniq_zero with p2; auto. split; auto. repeat split; auto. intros H7; case H4; apply uniq_opp; rewrite add_comm; auto. intros H7; case H1; apply uniq_zero with p2; auto. split; auto. case (ceqb p2 (add p1 p2)); intros H8. pattern p1 at 1; rewrite (uniq_zero _ (sym_equal H8)). rewrite <- H8; auto. case (ceqb p1 p2); intros H9. subst p1; apply add_comm. apply spec2_assoc; repeat split; auto. repeat split; auto. repeat split; auto. intros H10; case H4; apply uniq_opp; rewrite add_comm; auto. intros H10; case H3; apply uniq_opp; auto. intros H10; case H5; rewrite H10; rewrite opp_opp; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith