Next: Max and min on Up: The Integers Previous: Boolean valued functions on

## Propositional relations on integers

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)
```

Lego
1998-06-15