X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fnat%2Fplus.ma;h=75268ffcb4336b3ca709e5134dd51ae00c350a88;hb=2dc6ec0db2156431948014a6498c9901f8759e39;hp=809288f2a7bb7d6be2f39ab211811db124164a0b;hpb=3532e6714b7d0ee10b692e41c356866cfab5c646;p=helm.git

diff --git a/helm/software/matita/nlibrary/nat/plus.ma b/helm/software/matita/nlibrary/nat/plus.ma
index 809288f2a..75268ffcb 100644
--- a/helm/software/matita/nlibrary/nat/plus.ma
+++ b/helm/software/matita/nlibrary/nat/plus.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "nat/nat.ma".
+include "nat/big_ops.ma".
 include "algebra/unital_magmas.ma".
 include "algebra/abelian_magmas.ma".
 
@@ -50,4 +50,6 @@ ndefinition plus_unital_magma_type: unital_magma_type.
   | napply O
   | #x; napply refl
   | #x; (* qua manca ancora l'hint *) napply (symm plus_abelian_magma_type) ]
-nqed.
\ No newline at end of file
+nqed.
+
+ndefinition big_plus ≝ λn.λf.big_op plus_magma_type n f O.
\ No newline at end of file