proposition: Lemma uint_of_string_nonnil s : uint_of_string s <> Some Nil.
proof: Proof. destruct s; simpl. - easy. - destruct (NilEmpty.uint_of_string s); [intros H | intros [=]]. apply uint_of_char_spec in H. now intuition subst. Qed.
imports: Decimal Ascii String