(* byte → naturali *)
definition nat_of_byte8 ≝ λb:byte8.16*(b8h b) + (b8l b).
-coercion cic:/matita/freescale/byte8/nat_of_byte8.con.
+coercion nat_of_byte8.
(* naturali → byte *)
definition byte8_of_nat ≝ λn.mk_byte8 (exadecim_of_nat (n/16)) (exadecim_of_nat n).