Definition pcmIntegerEncodeSigned
  (depth     : nat)
  (amplitude : R)
: R :=
  match Rle_dec 0 amplitude with
  | left _  => Rmult amplitude ((pow 2 (depth - 1)) - 1)
  | right _ => Rmult amplitude (pow 2 (depth - 1))
  end.
