Propositional Strict Inequality

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_not_Eq = ... : {x,y:nat}(Lt x y)->not (Eq x y)
  Lt_zero = ... : {n:nat}(not (Eq n zero))->Lt zero n
  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
  Lt_pred = ... : {a,b|nat}(Lt a b)->Lt (pred b) b
  Lt_suc_pred = ... : {a,b|nat}(Lt (suc a) b)->Lt a (pred b)
  Lt_not_zero = ... : {a,b|nat}(Lt a b)->not (Eq b zero)
  Lt_pred_suc = ... : {a,b|nat}(Lt a (pred b))->Eq b (suc (pred b))
  Lt_pred_suc' = ... : {a,b|nat}(Lt (pred a) b)->Lt a (suc b)
  Lt_pred_suc'' = ... : {a,b|nat}(Lt a (pred b))->Lt (suc a) b
  n_Lt_suc_m_character = ... :
    {n,m|nat}(Lt n (suc m))->(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](Lt t (suc n) /\ P t)))
     (Ex ([t:nat](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}(Lt x n \/ (Eq x n /\ Lt y m))->P x y)->P n m)->
    {n,m:nat}P n m