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