Boolean valued functions on the integers

This file defines equality, strict and non-strict inequality as boolean valued functions. It also defines the boolean valued test for zero and positive and proves some theorems about them.

 ** Module lib_int_bool Imports lib_int_Prop_rels lib_nat_rels
  int_eq_zero = ... : int.1->bool
  int_Le_bool = ... : int.1->int.1->bool
  int_eq_bool = ... : int.1->int.1->bool
  int_Lt_bool = ... : int.1->int.1->bool
  bool_pos = ... : int.1->bool
  bool_pos_true_imp_pos = ... :
    {x:int.1}(Eq (bool_pos x) true)->Le_zed zero_zed x
  bool_pos_false_imp_pos = ... :
    {x:int.1}(Eq (bool_pos x) false)->Lt_zed x zero_zed
  pos_imp_bool_pos_true = ... :
    {x:int.1}(Le_zed zero_zed x)->Eq (bool_pos x) true
  pos_imp_bool_pos_false = ... :
    {x:int.1}(Lt_zed x zero_zed)->Eq (bool_pos x) false