X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Farithmetics%2Fminimization.ma;h=42767f66cc888dc8b89e2c10f33b535f672cd929;hb=f1c3f85a4e5acf2b6ee52b16103cbb95322016ac;hp=cb6eef689691578c607cf74569e3f36198cbe0fb;hpb=e7264f953fcf2cd2bef9057d83add08996d2ce75;p=helm.git

diff --git a/helm/software/matita/nlibrary/arithmetics/minimization.ma b/helm/software/matita/nlibrary/arithmetics/minimization.ma
index cb6eef689..42767f66c 100644
--- a/helm/software/matita/nlibrary/arithmetics/minimization.ma
+++ b/helm/software/matita/nlibrary/arithmetics/minimization.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "arithmetics/natsa.ma".
+include "arithmetics/nat.ma".
       
 nlet rec max i f ≝
   match i with 
@@ -235,4 +235,4 @@ ntheorem le_min_aux_r : ∀f:nat → bool.
   ∀off,n:nat. min_aux off n f ≤ n+off.
 #f; #off; nelim off; //;
 #n; #Hind; #a; nelim (min_aux_S f n a); *; /2/;
-nqed.
\ No newline at end of file
+nqed.