Commit 2026-01-30 10:38 cf59390d

feat(Data/Nat/Init): add div/mod extension theorems. (#34201) We don't actually have the theorems that directly state that div and mod form an injective pair in the natural way, despite having basically every other form of that statement that I can think of - and this form is quite a useful one. This PR adds these theorems and corresponding ModEq ones for good measure.