proposition: Lemma to_nat_bounded x : to_nat x <= 255.
proof: Proof. generalize (to_of_nat_option_map (to_nat x)). rewrite of_to_nat; cbn [option_map]. destruct (Nat.leb (to_nat x) 255) eqn:H; [ | congruence ]. rewrite (PeanoNat.Nat.leb_le (to_nat x) 255) in H. intro; assumption. Qed.
imports: Coq.Arith.EqNat Coq.NArith.BinNat Coq.NArith.Nnat Coq.Init.Byte