significant : (v : Integer) -> Nat -> {auto 0 _ : 0 <= v} -> (Integer, Nat)Extract the `n` most significant digits from a
non-negative integer plus the exponent representing
the remaining digits.
For example, for `v = 123456789` and `n = 3`, this
would return `(123,5)`, so that `v ~ 123 * 10^5`.