(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Z/sigma_p.ma".
+set "baseuri" "cic:/matita/Z/sigma_p".
include "Z/times.ma".
include "nat/primes.ma".
[intros.reflexivity
|intros.apply sym_Ztimes
]
-qed.
\ No newline at end of file
+qed.