In this file we define the order relations on integers and prove a number of theorems about them.
** Module lib_int_Prop_rels Imports lib_int_basics_thms lib_nat_Prop_rels Le_zed = ... : int.1->int.1->Prop Lt_zed = ... : int.1->int.1->Prop Le_resp_eq_l = ... : {a,b,x:int.1}(eq a b)->(Le_zed a x)->Le_zed b x Le_resp_eq_r = ... : {a,b,x:int.1}(eq a b)->(Le_zed x a)->Le_zed x b Lt_resp_eq_l = ... : {a,b,x:int.1}(eq a b)->(Lt_zed a x)->Lt_zed b x Lt_resp_eq_r = ... : {a,b,x:int.1}(eq a b)->(Lt_zed x a)->Lt_zed x b prod_pos_is_pos = ... : {x,y:zed}(Lt_zed zero_zed x)->(Lt_zed zero_zed y)-> Lt_zed zero_zed (times_zed x y) pos_imp_non_zero = ... : {x:int.1}(Lt_zed zero_zed x)->not (eq x zero_zed) eq_imp_Le_zed = ... : {x,y:int.1}(eq x y)->Le_zed x y Le_resp_times_zed = ... : {x,y,z:int.1}(Le_zed x y)->(Le_zed zero_zed z)-> Le_zed (times_zed z x) (times_zed z y) Lt_resp_times_zed = ... : {x,y,z:int.1}(Lt_zed x y)->(Lt_zed zero_zed z)-> Lt_zed (times_zed z x) (times_zed z y) Le_times_cancel_left_zed = ... : {x,y,a:int.1}(Lt_zed zero_zed a)-> (Le_zed (times_zed a x) (times_zed a y))->Le_zed x y Lt_times_cancel_left_zed = ... : {x,y,a:int.1}(Lt_zed zero_zed a)-> (Lt_zed (times_zed a x) (times_zed a y))->Lt_zed x y Lt_on_neg = ... : {x,y:int.1}(Lt_zed x y)->Lt_zed (neg_zed y) (neg_zed x) Lt_on_neg_rev = ... : {x,y:int.1}(Lt_zed (neg_zed y) (neg_zed x))->Lt_zed x y Le_on_neg = ... : {x,y:int.1}(Le_zed x y)->Le_zed (neg_zed y) (neg_zed x) Le_on_neg_rev = ... : {x,y:int.1}(Le_zed (neg_zed y) (neg_zed x))->Le_zed x y Le_antisym_zed = ... : {x,y:int.1}(Le_zed x y)->(Le_zed y x)->eq y x Le_trans_zed = ... : {x,y,z:int.1}(Le_zed x y)->(Le_zed y z)->Le_zed x z not_refl_Lt_zed = ... : {x:int.1}not (Lt_zed x x) Lt_trans_zed = ... : {x,y,z:int.1}(Lt_zed x y)->(Lt_zed y z)->Lt_zed x z Le_Lt_trans_zed = ... : {x,y,z:int.1}(Le_zed x y)->(Lt_zed y z)->Lt_zed x z Lt_Le_trans_zed = ... : {x,y,z:int.1}(Lt_zed x y)->(Le_zed y z)->Lt_zed x z Le_resp_plus_both_zed = ... : {x,y,a,b:int.1}(Le_zed x y)->(Le_zed a b)-> Le_zed (plus_zed x a) (plus_zed y b) Lt_resp_plus_both_zed = ... : {x,y,a,b:int.1}(Lt_zed x y)->(Lt_zed a b)-> Lt_zed (plus_zed x a) (plus_zed y b) Lt_resp_plus_zed = ... : {x,y,z:int.1}(Lt_zed x y)->Lt_zed (plus_zed z x) (plus_zed z y) prod_Le_is_pos = ... : {x,y:zed}(Le_zed zero_zed x)->(Le_zed zero_zed y)-> Le_zed zero_zed (times_zed x y) decide_int = ... : {x,y:int.1}(Le_zed x y \/ Lt_zed y x) Le_is_Lt_or_Eq_zed = ... : {x,y:int.1}(Le_zed x y)->(Lt_zed x y \/ eq x y) Le_resp_times_zed_neg = ... : {x,y,z:int.1}(Le_zed x y)->(Lt_zed z zero_zed)-> Le_zed (times_zed z y) (times_zed z x)