feat(data/fin/basic): coe_sub_iff_{le,lt} (#15930)
Also clean up the `order_dual` definition and proofs.
Add
```
nat.mod_eq_iff_lt
@[simp] nat.mod_succ_eq_iff_lt
```
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
