+ intro;
+ unfold byte_of_nat;
+ apply eq_f2;
+ [ rewrite > exadecimal_of_nat_mod in ⊢ (? ? % ?);
+ rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
+ apply eq_f;
+ elim daemon
+ | rewrite > exadecimal_of_nat_mod;
+ rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
+ rewrite > divides_to_eq_mod_mod_mod;
+ [ reflexivity
+ | autobatch
+ ]
+ ]
+qed.