Propositional relations on integers

In this file we define the order relations on integers and prove a number of theorems about them.

 ** Module lib_int_Prop_rels Imports lib_integers/lib_int_basics_thms
     lib_nat/lib_nat_Prop_rels
  Le_zed = ... : int.1->int.1->Prop
  Lt_zed = ... : int.1->int.1->Prop
  Le_resp_eq_l = ... : {a,b,x:int.1}(eq a b)->(Le_zed a x)->Le_zed b x
  Le_resp_eq_r = ... : {a,b,x:int.1}(eq a b)->(Le_zed x a)->Le_zed x b
  Lt_resp_eq_l = ... : {a,b,x:int.1}(eq a b)->(Lt_zed a x)->Lt_zed b x
  Lt_resp_eq_r = ... : {a,b,x:int.1}(eq a b)->(Lt_zed x a)->Lt_zed x b
  prod_pos_is_pos = ... :
    {x,y:zed}(Lt_zed zero_zed x)->(Lt_zed zero_zed y)->
    Lt_zed zero_zed (times_zed x y)
  pos_imp_non_zero = ... :
    {x:int.1}(Lt_zed zero_zed x)->not (eq x zero_zed)
  eq_imp_Le_zed = ... : {x,y:int.1}(eq x y)->Le_zed x y
  Le_resp_times_zed = ... :
    {x,y,z:int.1}(Le_zed x y)->(Le_zed zero_zed z)->
    Le_zed (times_zed z x) (times_zed z y)
  Lt_resp_times_zed = ... :
    {x,y,z:int.1}(Lt_zed x y)->(Lt_zed zero_zed z)->
    Lt_zed (times_zed z x) (times_zed z y)
  Le_times_cancel_left_zed = ... :
    {x,y,a:int.1}(Lt_zed zero_zed a)->
    (Le_zed (times_zed a x) (times_zed a y))->Le_zed x y
  Lt_times_cancel_left_zed = ... :
    {x,y,a:int.1}(Lt_zed zero_zed a)->
    (Lt_zed (times_zed a x) (times_zed a y))->Lt_zed x y
  Lt_on_neg = ... :
    {x,y:int.1}(Lt_zed x y)->Lt_zed (neg_zed y) (neg_zed x)
  Lt_on_neg_rev = ... :
    {x,y:int.1}(Lt_zed (neg_zed y) (neg_zed x))->Lt_zed x y
  Le_on_neg = ... :
    {x,y:int.1}(Le_zed x y)->Le_zed (neg_zed y) (neg_zed x)
  Le_on_neg_rev = ... :
    {x,y:int.1}(Le_zed (neg_zed y) (neg_zed x))->Le_zed x y
  Le_antisym_zed = ... : {x,y:int.1}(Le_zed x y)->(Le_zed y x)->eq y x
  Le_trans_zed = ... :
    {x,y,z:int.1}(Le_zed x y)->(Le_zed y z)->Le_zed x z
  not_refl_Lt_zed = ... : {x:int.1}not (Lt_zed x x)
  Lt_trans_zed = ... :
    {x,y,z:int.1}(Lt_zed x y)->(Lt_zed y z)->Lt_zed x z
  Le_Lt_trans_zed = ... :
    {x,y,z:int.1}(Le_zed x y)->(Lt_zed y z)->Lt_zed x z
  Lt_Le_trans_zed = ... :
    {x,y,z:int.1}(Lt_zed x y)->(Le_zed y z)->Lt_zed x z
  Le_resp_plus_both_zed = ... :
    {x,y,a,b:int.1}(Le_zed x y)->(Le_zed a b)->
    Le_zed (plus_zed x a) (plus_zed y b)
  Lt_resp_plus_both_zed = ... :
    {x,y,a,b:int.1}(Lt_zed x y)->(Lt_zed a b)->
    Lt_zed (plus_zed x a) (plus_zed y b)
  Lt_resp_plus_zed = ... :
    {x,y,z:int.1}(Lt_zed x y)->Lt_zed (plus_zed z x) (plus_zed z y)
  prod_Le_is_pos = ... :
    {x,y:zed}(Le_zed zero_zed x)->(Le_zed zero_zed y)->
    Le_zed zero_zed (times_zed x y)
  decide_int = ... : {x,y:int.1}or (Le_zed x y) (Lt_zed y x)
  Le_is_Lt_or_Eq_zed = ... :
    {x,y:int.1}(Le_zed x y)->or (Lt_zed x y) (eq x y)
  Le_resp_times_zed_neg = ... :
    {x,y,z:int.1}(Le_zed x y)->(Lt_zed z zero_zed)->
    Le_zed (times_zed z y) (times_zed z x)