Lemma mod_sub : forall x m,
  0 < m -> 0 < m - (x mod m) <= m.
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.
