DPD trailing-field bounds and round trips

Packing groups declets produces a value below 1024 ^ groups; decoding produces a coefficient below 1000 ^ groups. Encoding then decoding recovers every coefficient within that bound, and canonicalization preserves the decoded trailing coefficient.

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.encodeTrailing_lt (groups n : ℕ) : encodeTrailing groups n < 1024 ^ groups

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.decodeTrailing_lt (groups n : ℕ) : decodeTrailing groups n < 1000 ^ groups

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.decodeTrailing_encodeTrailing (groups n : ℕ) (h : n < 1000 ^ groups) : decodeTrailing groups (encodeTrailing groups n) = n

Packing followed by unpacking preserves every trailing decimal digit.

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.decodeTrailing_canonicalize (groups n : ℕ) : decodeTrailing groups (encodeTrailing groups (decodeTrailing groups n)) = decodeTrailing groups n

Canonicalizing redundant declets preserves the complete trailing coefficient.