The final file for natural numbers defines the functions max and min and proves various theorems about them. It requires most of the other nat library files. The functions min and max are defined explicitly using double iteration rather than by showing that the order relation on nat is complete.
** Module lib_max_min Imports lib_nat_Prop_rels max = ... : nat->nat->nat min = ... : nat->nat->nat max_Le_left = ... : {x,y:nat}Le x (max x y) max_Le_right = ... : {x,y:nat}Le y (max x y) max_is_least = ... : {x,y,z:nat}(Le x z)->(Le y z)->Le (max x y) z min_Le_left = ... : {x,y:nat}Le (min x y) y min_Le_right = ... : {x,y:nat}Le (min x y) x min_is_greatest = ... : {x,y,z:nat}(Le z x)->(Le z y)->Le z (min x y) max_sym = ... : {n,m:nat}Eq (max n m) (max m n) max_assoc = ... : {m,n,o:nat}Eq (max (max m n) o) (max m (max n o)) max_suc_pred = ... : {m,n:nat}Eq (max m (suc n)) (suc (max (pred m) n)) min_sym = ... : {n,m:nat}Eq (min n m) (min m n) Le_min_left = ... : {x,y:nat}(Le x y)->Eq (min x y) x Le_min_right = ... : {x,y:nat}(Le y x)->Eq (min x y) y Le_max_right = ... : {x,y:nat}(Le x y)->Eq (max x y) y Le_max_left = ... : {x,y:nat}(Le y x)->Eq (max x y) x min_idemp = ... : {a:nat}Eq (min a a) a max_resp_times = ... : {x,y,a:nat}Eq (max (times a x) (times a y)) (times a (max x y)) min_resp_times = ... : {x,y,a:nat}Eq (min (times a x) (times a y)) (times a (min x y)) max_resp_plus = ... : {a,b,x:nat}Eq (max (plus a x) (plus b x)) (plus (max a b) x) min_resp_plus = ... : {a,b,x:nat}Eq (min (plus a x) (plus b x)) (plus (min a b) x)