Next: Propositional Relations Up: Order relations Previous: Propositional Inequality

### 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
```

Conor McBride
11/13/1998