For integer e>=1, x^e-y^e=(x-y)*sum(j<e,x^(e-1-j)*y^j); if |x|,|y|<=H, then |x^e-y^e|<=e*H^(e-1)*|x-y|. Treat e=0 separately.
Method: native-induction. Induction: e. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.