+ lapply (eqex_true_to_eq ? ? H1); clear H1;
+ unfold byte_of_nat in Hletin;
+ change in Hletin with (exadecimal_of_nat (S a) = x0);
+ lapply (eq_f ? ? nat_of_exadecimal ? ? Hletin); clear Hletin;
+ normalize in Hletin1:(? ? ? %);
+ rewrite > nat_of_exadecimal_exadecimal_of_nat in Hletin1;
+ elim (eq_mod_O_to_exists ? ? Hletin1); clear Hletin1;
+ rewrite > H1;
+ rewrite > lt_O_to_div_times; [2: autobatch | ]
+ lapply (eq_f ? ? (λx.x/16) ? ? H1);
+ rewrite > lt_O_to_div_times in Hletin; [2: autobatch | ]
+ lapply (eq_f ? ? (λx.x \mod 16) ? ? H1);
+ rewrite > eq_mod_times_n_m_m_O in Hletin1;
+ elim daemon
+ | change with (mk_byte (bh (byte_of_nat (S a))) (xpred (bl (byte_of_nat (S a))))
+ = byte_of_nat a);
+ unfold byte_of_nat;
+ change with (mk_byte (exadecimal_of_nat (S a/16)) (xpred (exadecimal_of_nat (S a)))
+ = mk_byte (exadecimal_of_nat (a/16)) (exadecimal_of_nat a));
+ lapply (eqex_false_to_not_eq ? ? H1);
+ unfold byte_of_nat in Hletin;
+ change in Hletin with (exadecimal_of_nat (S a) ≠ x0);
+ cut (nat_of_exadecimal (exadecimal_of_nat (S a)) ≠ 0);
+ [2: intro;
+ apply Hletin;
+ lapply (eq_f ? ? exadecimal_of_nat ? ? H2);
+ rewrite > exadecimal_of_nat_nat_of_exadecimal in Hletin1;
+ apply Hletin1
+ | ];
+
+ elim daemon
+ ]