proposition: Lemma sus s d : uint_of_string s = Some d -> string_of_uint d = s.
proof: Proof. revert d. induction s; simpl. - now intros d [= <-]. - intros d. destruct (uint_of_string s); [intros H | intros [=]]. apply uint_of_char_spec in H. intuition subst; simpl; f_equal; auto. Qed.
imports: Decimal Ascii String