feat(NumberTheory/EllipticDivisibilitySequence): extend even-odd recursion to integers (#13786)

Provide a quick proof that normalised EDSs satisfy an even-odd recursion over all integers rather than just natural numbers, without relying on heavier machinery i.e. the full EDS recurrence in #13155, and make `Int.negInduction` slightly stronger.

Author: Multramate