(* *)
(**************************************************************************)
-include "arithmetics/natsa.ma".
+include "arithmetics/nat.ma".
nlet rec max i f ≝
match i with
∀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.