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

[R J]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090315/253b7a82/attachment.htm