no admitted lemmas. Changed nat_to_string implementation