(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Z/sigma_p".
-
include "Z/times.ma".
include "nat/primes.ma".
include "nat/ord.ma".
apply (iter_p_gen_plusA Z n k p g OZ Zplus)
[ apply symmetricZPlus.
| intros.
- apply cic:/matita/Z/plus/Zplus_z_OZ.con
+ apply Zplus_z_OZ.
| apply associative_Zplus
]
qed.