Propositional Inequality

The order relation $\leq$ 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_times_thms 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))->(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)
  Le_suc_pred = ... : {a,b|nat}(Le (suc a) b)->Le a (pred b)
  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)