proposition: Lemma usu_gen d : uint_of_string (string_of_uint d) = Some d \/ uint_of_string (string_of_uint d) = Some Hexadecimal.zero.
proof: Proof. destruct d; (now right) || (left; now apply usu). Qed.
imports: Hexadecimal Ascii String