proposition: Lemma isi d : int_of_string (string_of_int d) = Some d.
proof: Proof. destruct d; simpl. - unfold int_of_string. destruct (string_of_uint d) eqn:Hd. + now destruct d. + case Ascii.eqb_spec. * intros ->. now destruct d. * rewrite <- Hd, usu; auto. - rewrite usu; auto. Qed.
imports: Decimal Ascii String