From 164e0005e806f5c995817cd0a494429ebac508d9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 23 Sep 2010 22:35:46 +0000 Subject: [PATCH] fix typo --- helm/software/matita/nlibrary/arithmetics/minimization.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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. -- 2.39.2