]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/RELATIONAL/Zah/setoid.ma
contribs: some improvements
[helm.git] / helm / software / matita / contribs / RELATIONAL / Zah / setoid.ma
index 8815ee5bb6e3bbc0314c1aa95dcca55d28fe4c18..e30b5a205723b3ae8cbad46098bdb2d1edc99989 100644 (file)
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/RELATIONAL/Zah/setoid".
 
-include "NPlus/props.ma".
+include "NPlus/monoid.ma".
 include "Zah/defs.ma".
 
 theorem nplus_total: \forall p,q. \exists r. p + q == r.
@@ -57,4 +57,4 @@ theorem zeq_trans: \forall z1,z2. z1 = z2 \to
  
  
 
-*)
\ No newline at end of file
+*)