This file defined the relations Divides, and Coprime and proves some properties of them.
** Module lib_int_number_theory Imports lib_integers/lib_int_mod
Divides = ... : zed->zed->Prop
Coprime = ... : zed->zed->Prop
refl_Divides = ... : refl Divides
divides_implies_is_zero_modulo = ... :
{m,n|int.1}(Divides m n)->Mod m n zero_zed
times_Divides = ... :
{m,n,p|int.1}(Divides m n)->Divides m (times_zed p n)
times_Divides' = ... :
{m,n,p|int.1}(Divides m p)->Divides m (times_zed p n)
sym_Coprime = ... : sym Coprime
factor_Coprime = ... :
{p,m,n|int.1}(Coprime p (times_zed m n))->Coprime p n
factor_Coprime' = ... :
{p,m,n|int.1}(Coprime p (times_zed m n))->Coprime p m