module Properties where
import Test3

symmetric r x y =
  r x y == r y x

transitive r x y z = 
  r x y && r y z ==> r x z

associative op x y z = x `op` (y `op` z) == (x `op` y) `op` z
commutative op x y = x `op` y == y `op` x
hasunit op e x = x`op`e == x && e`op`x == x
haszero op z x = x`op`z == z && z`op`x == z

monotonic f x y = x<=y ==> f x<=f y
isUB f x y = x <= f x y
isLB f x y = f x y <= x

extensionally r f g x = r (f x) (g x)
f\==g = extensionally (==) f g

ordered xs = and (zipWith (<=) xs (drop 1 xs))