proposition: Lemma to_N_bounded x : to_N x <= 255.
proof: Proof. generalize (to_of_N_option_map (to_N x)). rewrite of_to_N; cbn [option_map]. destruct (N.leb (to_N x) 255) eqn:H; [ | congruence ]. rewrite (N.leb_le (to_N x) 255) in H. intro; assumption. Qed.
imports: Coq.Arith.EqNat Coq.NArith.BinNat Coq.NArith.Nnat Coq.Init.Byte