`NUMBER_RULE : term -> thm`

SYNOPSIS
Automatically prove elementary divisibility property over the natural numbers.

DESCRIPTION
NUMBER_RULE is a partly heuristic rule that can often automatically prove elementary ``divisibility'' properties of the natural numbers. The precise subset that is dealt with is difficult to describe rigorously, but many universally quantified combinations of divides, coprime, gcd and congruences (x == y) (mod n) can be proved automatically, as well as some existentially quantified goals. See a similar rule INTEGER_RULE for the integers for a representative set of examples.

FAILURE CONDITIONS
Fails if the goal is not accessible to the methods used.

EXAMPLE
Here is a typical example, which would be rather tedious to prove manually:
```  # NUMBER_RULE
`!a b a' b'. ~(gcd(a,b) = 0) /\ a = a' * gcd(a,b) /\ b = b' * gcd(a,b)
==> coprime(a',b')`;;
...
val it : thm =
|- !a b a' b'.
~(gcd (a,b) = 0) /\ a = a' * gcd (a,b) /\ b = b' * gcd (a,b)
==> coprime (a',b')
```