Strict inequality is defined in the next file. A very similar collection of theorems is given to those above, with the addition of a couple of extra induction principles. These are in this file mainly because at this point all the necessary lemmas are available.
** Module lib_nat_Lt Imports lib_nat_minus_thms
Lt = ... : nat->nat->Prop
zero_Lt_suc_n = ... : {n:nat}Lt zero (suc n)
n_Lt_suc_n = ... : {n:nat}Lt n (suc n)
Lt_trans = ... : {l,m,n|nat}(Lt l m)->(Lt m n)->Lt l n
not_n_Lt_zero = ... : {n:nat}not (Lt n zero)
not_refl_Lt = ... : {x:nat}not (Lt x x)
Lt_resp_suc = ... : {m,n:nat}(Lt m n)->Lt (suc m) (suc n)
Lt_resp_pred = ... : {x,y:nat}(Lt (suc x) (suc y))->Lt x y
n_Lt_suc_m_character = ... :
{n,m|nat}(Lt n (suc m))->or (Lt n m) (Eq n m)
plus_resp_Lt_l = ... :
{l,m|nat}(Lt l m)->{n:nat}Lt (plus l n) (plus m n)
Lt_resp_plus = ... : {x,y,z:nat}(Lt x y)->Lt (plus z x) (plus z y)
Lt_resp_plus_both = ... :
{x,y,a,b:nat}(Lt x y)->(Lt a b)->Lt (plus x a) (plus y b)
Lt_resp_plus_right = ... : {a,x,y|nat}(Lt x y)->Lt x (plus a y)
Lt_resp_times = ... :
{x,y,a:nat}(Lt x y)->Lt (times (suc a) x) (times (suc a) y)
Lt_resp_sub = ... : {x,y,z:nat}(Lt (plus z x) (plus z y))->Lt x y
Lt_times_cancel = ... :
{x,y,a:nat}(Lt (times x (suc a)) (times y (suc a)))->Lt x y
ze_Lt_imp_Eq_suc = ... : {m:nat}(Lt zero m)->Ex ([n:nat]Eq m (suc n))
exists_suc = ... :
{P:nat->Prop}{n:nat}
iff (Ex ([t:nat]and (Lt t (suc n)) (P t)))
(or (Ex ([t:nat]and (Lt t n) (P t))) (P n))
complete_induction = ... :
{P:nat->Prop}({n:nat}({x:nat}(Lt x n)->P x)->P n)->{m:nat}P m
well_founded_induction = ... :
{t|Type}{f:t->nat}{P:t->Prop}
({x:t}({y:t}(Lt (f y) (f x))->P y)->P x)->{z:t}P z
nested_complete_induction = ... :
{P:nat->nat->Prop}
({n,m:nat}({x,y:nat}(or (Lt x n) (and (Eq x n) (Lt y m)))->P x y)->
P n m)->{n,m:nat}P n m