Max and min on integers

In this section max and min are defined on integers and a number of theorems proved about them.

 ** Module lib_int_max_min Imports lib_int_basics_thms lib_int_Prop_rels
     lib_max_min
  min_zed = ... : int.1->int.1->int.1
  max_zed = ... : int.1->int.1->int.1
  max_resp_eq = ... :
    {a,b,x,y:int.1}(eq a b)->(eq x y)->eq (max_zed a x) (max_zed b y)
  min_resp_eq = ... :
    {a,b,x,y:int.1}(eq a b)->(eq x y)->eq (min_zed a x) (min_zed b y)
  max_Le_left_zed = ... : {x,y:int.1}Le_zed x (max_zed x y)
  max_Le_right_zed = ... : {x,y:int.1}Le_zed y (max_zed x y)
  min_Le_left_zed = ... : {x,y:int.1}Le_zed (min_zed x y) x
  min_Le_right_zed = ... : {x,y:int.1}Le_zed (min_zed x y) y
  max_is_least_zed = ... :
    {x,y,z:int.1}(Le_zed x z)->(Le_zed y z)->Le_zed (max_zed x y) z
  min_is_greatest_zed = ... :
    {x,y,z:int.1}(Le_zed z x)->(Le_zed z y)->Le_zed z (min_zed x y)
  max_resp_plus_zed = ... :
    {x,y,z:int.1}
    eq (max_zed (plus_zed z x) (plus_zed z y))
     (plus_zed z (max_zed x y))
  min_resp_plus_zed = ... :
    {x,y,z:int.1}
    eq (min_zed (plus_zed z x) (plus_zed z y))
     (plus_zed z (min_zed x y))
  Le_min_left_zed = ... : {x,y:int.1}(Le_zed x y)->eq (min_zed x y) x
  Le_min_right_zed = ... : {x,y:int.1}(Le_zed y x)->eq (min_zed x y) y
  Le_max_right_zed = ... : {x,y:int.1}(Le_zed x y)->eq (max_zed x y) y
  Le_max_left_zed = ... : {x,y:int.1}(Le_zed y x)->eq (max_zed x y) x
  max_resp_times_zed = ... :
    {x,y,a:int.1}(Le_zed zero_zed a)->
    eq (max_zed (times_zed a x) (times_zed a y))
     (times_zed a (max_zed x y))
  min_resp_times_zed = ... :
    {x,y,a:int.1}(Le_zed zero_zed a)->
    eq (min_zed (times_zed a x) (times_zed a y))
     (times_zed a (min_zed x y))
  max_sym_zed = ... : {x,y:int.1}eq (max_zed x y) (max_zed y x)
  min_sym_zed = ... : {x,y:int.1}eq (min_zed x y) (min_zed y x)
  min_zed_idemp = ... : {a|zed}Eq_zed (min_zed a a) a