next up previous contents
Next: The predicate Even Up: The Natural Numbers Previous: Boolean-valued Relations

All order relations

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

Fri May 24 19:01:27 BST 1996