proposition: Theorem pplus_assoc: forall p q r, (pplus p (pplus q r)) = (pplus (pplus p q) r).
proof: Proof. intros p q r; case p; case q; case r; intros r1 r2 q1 q2 p1 p2; unfold pplus. eq_tac; ring. Qed.
imports: ZArith Znumtheory Tactic Wf_nat ListAux UList FGroup EGroup IGroup