# INTEGER_RULE
`!x y n:int. (x == y) (mod n) ==> (n divides x <=> n divides y)`;;
...
val it : thm = |- !x y n. (x == y) (mod n) ==> (n divides x <=> n divides y)
# INTEGER_RULE
`!a b d:int. d divides gcd(a,b) <=> d divides a /\ d divides b`;;
...
val it : thm =
|- !a b d. d divides gcd (a,b) <=> d divides a /\ d divides b

including some less obvious ones:
# INTEGER_RULE
`!x y. coprime(x * y,x pow 2 + y pow 2) <=> coprime(x,y)`;;
...
val it : thm = |- !x y. coprime (x * y,x pow 2 + y pow 2) <=> coprime (x,y)

A limited class of existential goals is solvable too, e.g. a classic
sufficient condition for a linear congruence to have a solution:
# INTEGER_RULE `!a b n:int. coprime(a,n) ==> ?x. (a * x == b) (mod n)`;;
...
val it : thm = |- !a b n. coprime (a,n) ==> (?x. (a * x == b) (mod n))

or the two-number Chinese Remainder Theorem:
# INTEGER_RULE
`!a b u v:int. coprime(a,b) ==> ?x. (x == u) (mod a) /\ (x == v) (mod b)`;;
...
val it : thm =
|- !a b u v. coprime (a,b) ==> (?x. (x == u) (mod a) /\ (x == v) (mod b))