The next file is very short in itself but it loads all the other order relation files. The theorems in it relate the propositional or logical relations with their boolean counterparts.
** Module lib_nat_rels Imports lib_nat/lib_nat_Prop_rels
lib_nat/lib_nat_bool_rels
le_true_imp_Le = ... : {n,m:nat}(Eq (le n m) true)->Le n m
le_false_imp_Lt = ... : {n,m:nat}(Eq (le n m) false)->Lt m n
Le_imp_le_true = ... : {n,m:nat}(Le n m)->Eq (le n m) true
Lt_imp_le_false = ... : {n,m:nat}(Lt m n)->Eq (le n m) false
lt_true_imp_Lt = ... : {n,m:nat}(Eq (lt n m) true)->Lt n m
lt_false_imp_Le = ... : {n,m:nat}(Eq (lt n m) false)->Le m n
Lt_imp_lt_true = ... : {n,m:nat}(Lt n m)->Eq (lt n m) true
Le_imp_lt_false = ... : {n,m:nat}(Le n m)->Eq (lt m n) false