next up previous contents
Next: The predicate Even Up: Order relations 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_Prop_rels 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

Conor McBride