[Haskell-cafe] A non-inductive Haskell proof?

The following theorem is obviously true, but how is it proved (most cleanly and simply) in Haskell? Theorem: (nondecreasing xs) => nondecreasing (insert x xs), where: nondecreasing :: (Ord a) => [a] -> Bool nondecreasing [] = True nondecreasing xxs@(x : xs) = and [a <= b | (a, b) <- zip xxs xs] insert :: (Ord a) => a -> [a] -> [a] insert x xs = takeWhile (<= x) xs ++ [x] ++ dropWhile (<= x) xs Thanks. _________________________________________________________________ Hotmail® is up to 70% faster. Now good news travels really fast. http://windowslive.com/online/hotmail?ocid=TXT_TAGLM_WL_HM_70faster_032009