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