proposition: Lemma sis s d : int_of_string s = Some d -> string_of_int d = s.
proof: Proof. destruct s; [intros [= <-]| ]; simpl; trivial. case Ascii.eqb_spec. - intros ->. destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-]. simpl; f_equal. now apply sus. - destruct d; [ | now destruct uint_of_char]. simpl string_of_int. intros. apply sus; simpl. destruct uint_of_char; simpl in *; congruence. Qed.
imports: Decimal Ascii String