feat: add `Nat.ext_div_mod` and `Int.ext_ediv_emod`

This PR adds theorems that directly state that div and mod form an
injective pair: if `a / n = b / n` and `a % n = b % n` then `a = b`.
These complement existing div/mod lemmas and are useful for extension
arguments.

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>