PrimeDividesByTheBinomialTheorem​(AngouriMath.​Entity,​AngouriMath.​Entity)

Whether p divides d by the binomial theorem, with the facts in scope: p is
prime, d is a polynomial with whole coefficients in whole quantities, and
writing each power (u + v)^p in it as u^p + v^p leaves nothing, or only
multiples of p. What the binomial theorem adds to u^p + v^p is
binomial(p, k) u^k v^(p - k) for 0 < k < p, each a multiple of
p by PrimeDividesItsBinomial(AngouriMath.Entity,AngouriMath.Entity). That is asked of the quantifiers
first, and recorded as the step this one rests on. A difference is read the same way,
since (-v)^p is -v^p modulo every prime, 2 included. Sullivan and
Mackey's Prob 8.9.25, the freshman's dream.