Some theorems about Modulo

This file defines the relation Modulo, and proves a couple of theorems about it.

 ** Module lib_int_mod Imports lib_int_basics_thms
  Mod = ... : int.1->int.1->int.1->Prop
  plus_resp_mod = ... :
    {m,x1,x2,r1,r2|int.1}(Mod m x1 r1)->(Mod m x2 r2)->
    Mod m (plus_zed x1 x2) (plus_zed r1 r2)
  times_resp_Mod = ... :
    {m,x1,x2,r1,r2|int.1}(Mod m x1 r1)->(Mod m x2 r2)->
    Mod m (times_zed x1 x2) (times_zed r1 r2)