The order relations on nat are decidable so another way to represent them is via boolean valued functions. The following file defines boolean-valued strict and non-strict inequality plus the boolean-valued equality. Most of the propositional order relation theorems have a boolean counterpart, the most useful of which are included in the library.
** Module lib_nat_bool_rels Imports lib_nat_suc_thms lib_bool_thms
lt = ... : nat->nat->bool
le = ... : nat->nat->bool
nat_eq = ... : nat->nat->bool
zero_lt_suc = ... : {n:nat}is_true (lt zero (suc n))
zero_le_suc = ... : {n:nat}is_true (le zero (suc n))
not_n_lt_zero = ... : {n:nat}is_false (lt n zero)
lt_resp_suc = ... : {n,m:nat}Eq (lt n m) (lt (suc n) (suc m))
le_resp_suc = ... : {n,m:nat}Eq (le n m) (le (suc n) (suc m))
not_n_lt_n = ... : {n:nat}is_false (lt n n)
n_lt_suc_n = ... : {n:nat}is_true (lt n (suc n))
not_lt_suc_is_suc = ... : {m,n:nat}(is_false (lt m (suc n)))->is_suc m
lt_weak_trans = ... :
{m,n|nat}(is_true (lt m n))->is_true (lt m (suc n))
lt_left_suc = ... :
{n,m:nat}(is_true (lt (suc n) m))->is_true (lt n m)
lt_suc_character = ... :
{m,n:nat}(is_true (lt n (suc m)))->(Eq n m \/ is_true (lt n m))
lt_character = ... :
{n,m:nat}
((is_true (lt n m) /\ is_false (lt m n)) \/
((is_true (lt m n) /\ is_false (lt n m)) \/ Eq n m))
le_character = ... :
{n,m:nat}
((is_true (le n m) /\ is_false (le m n)) \/
((is_true (le m n) /\ is_false (le n m)) \/ Eq n m))
le_refl = ... : {n:nat}is_true (le n n)
le_zero_imp_zero = ... : {n:nat}iff (is_true (le n zero)) (Eq n zero)
le_not_lt_imp_Eq = ... :
{i,n:nat}(is_true (le i n) /\ is_false (lt i n))->Eq i n
lt_imp_le_suc = ... :
{x,y|nat}(is_true (lt x y))->is_true (le (suc x) y)
nat_eq_character = ... : {m,n:nat}iff (is_true (nat_eq m n)) (Eq m n)
nat_eq_character' = ... :
{m,n:nat}iff (is_false (nat_eq m n)) (not (Eq m n))
nat_eq_sym = ... : {m,n:nat}Eq (nat_eq m n) (nat_eq n m)
nat_eq_refl = ... : {n:nat}is_true (nat_eq n n)
odd = ... : nat->bool
even = ... : nat->bool