This file incorporates both propositional inequalities and gives several additional theorems involving both inequalities.
** Module lib_nat_Prop_rels Imports lib_nat_Lt lib_nat_Le
Lt_Le_trans = ... : {x,y,z|nat}(Lt x y)->(Le y z)->Lt x z
Le_Lt_trans = ... : {x,y,z|nat}(Le x y)->(Lt y z)->Lt x z
Lt_imp_Le = ... : {x,y:nat}(Lt x y)->Le x y
Lt_Le_resp_plus = ... :
{x,y,a,b:nat}(Lt x y)->(Le a b)->Lt (plus x a) (plus y b)
Le_Lt_resp_plus = ... :
{x,y,a,b:nat}(Le x y)->(Lt a b)->Lt (plus x a) (plus y b)
decide_nat = ... : {x,y:nat}(Le x y \/ Lt y x)
Le_is_Lt_or_Eq = ... : {x,y:nat}(Le x y)->(Lt x y \/ Eq x y)
zero_or_pos = ... : {n:nat}(Eq n zero \/ Lt zero n)
Lt_imp_Le_suc = ... : {x,y:nat}(Lt x (suc y))->Le x y
Le_imp_Lt_suc = ... : {x,y:nat}(Le x y)->Lt x (suc y)
Lt_resp_times_both = ... :
{x,y,a,b:nat}(Lt x y)->(Lt a b)->Lt (times a x) (times b y)
Lt_imp_Le_suc' = ... : {x,y:nat}(Lt x y)->Le (suc x) y
Le_imp_Lt_suc' = ... : {x,y:nat}(Le (suc x) y)->Lt x y
minus_well_le = ... :
{m,n:nat}(Lt zero m)->(Le m n)->Lt (plus (minus n m) m) (plus n m)
not_Le_imp_Lt = ... : {x,y:nat}(not (Le x y))->Lt y x
not_Lt_imp_Le = ... : {x,y:nat}(not (Lt x y))->Le y x
Le_minus_zero = ... : {a,b:nat}(Le a b)->Eq (minus a b) zero
Le_resp_minus = ... : {a,b,c:nat}(Le a b)->Le (minus c b) (minus c a)