proposition: Lemma to_of_N_option_map x : option_map to_N (of_N x) = if N.leb x 255 then Some x else None.
proof: Proof. cbv [of_N]; repeat match goal with | [ |- context[match ?x with _ => _ end] ] => is_var x; destruct x end; reflexivity. Qed.
imports: Coq.Arith.EqNat Coq.NArith.BinNat Coq.NArith.Nnat Coq.Init.Byte