restored deleted proof

Author: jamesmckinna

src/Data/Digit.agda

@@ -56,7 +56,7 @@ toNatDigits base@(suc (suc _)) n = aux (<-wellFounded-fast n) []
   aux {zero}        _      xs =  (0 ∷ xs)
   aux {n@(suc _)} (acc wf) xs with does (0 <? n / base)
   ... | false = (n % base) ∷ xs -- n here is already sufficient?
-  ... | true  = aux (wf (m/n<m n base)) ((n % base) ∷ xs)
+  ... | true  = aux (wf (m/n<m n base sz<ss)) ((n % base) ∷ xs)
 
 ------------------------------------------------------------------------
 -- Converting between `ℕ` and expansions of `Digit base`