rewrite > nat_of_exadecimal_exadecimal_of_nat in Hletin1;
elim (eq_mod_O_to_exists ? ? Hletin1); clear Hletin1;
rewrite > H1;
rewrite > nat_of_exadecimal_exadecimal_of_nat in Hletin1;
elim (eq_mod_O_to_exists ? ? Hletin1); clear Hletin1;
rewrite > H1;