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