The order relation 
is defined in one file, with
its associated theorems. There is some redundancy e.g.
Le_resp_plus is trivially implied by
Le_resp_plus_both.
Having both theorems available is useful in further
development.
** Module lib_nat_Le Imports lib_nat/lib_nat_times_thms
lib_nat/lib_nat_minus_thms
Le = ... : nat->nat->Prop
Le_plus_lemma1 = ... : {m,n|nat}Le m (plus m n)
Le_plus_lemma2 = ... : {m,n|nat}Le n (plus m n)
Le_suc_lemma = ... :
{m,n|nat}(Le m (suc n))->or (Le m n) (Eq (suc n) m)
Le_antisym = ... : {m,n:nat}(Le m n)->(Le n m)->Eq n m
Le_suc = ... : {x:nat}Le x (suc x)
Le_resp_suc = ... : {x,y:nat}(Le x y)->Le (suc x) (suc y)
Le_resp_pred = ... : {x,y:nat}(Le (suc x) (suc y))->Le x y
Le_zero_n = ... : {n:nat}Le zero n
Le_incl_pred = ... : {x:nat}Le (pred x) x
not_Le_zero_n = ... : {n:nat}not (Le (suc n) zero)
eq_imp_Le = ... : {x,y:nat}(Eq x y)->Le x y
Le_trans = ... : {x,y,z|nat}(Le x y)->(Le y z)->Le x z
Le_resp_plus = ... : {x,y,z:nat}(Le x y)->Le (plus z x) (plus z y)
Le_resp_sub = ... : {x,y,z:nat}(Le (plus z x) (plus z y))->Le x y
Le_resp_plus_both = ... :
{x,y,a,b:nat}(Le x y)->(Le a b)->Le (plus x a) (plus y b)
Le_resp_times = ... : {x,y,a:nat}(Le x y)->Le (times a x) (times a y)
Le_times_cancel = ... :
{x,y,a:nat}(Le (times x (suc a)) (times y (suc a)))->Le x y
Le_resp_times_both = ... :
{a,b,x,y:nat}(Le a b)->(Le x y)->Le (times a x) (times b y)
plus_inv_minus = ... : {m,n:nat}(Le m n)->Eq n (plus (minus n m) m)