proposition: Lemma to_of_nat_option_map x : option_map to_nat (of_nat x) = if Nat.leb x 255 then Some x else None.
proof: Proof. do 256 try destruct x as [|x]; reflexivity. Qed.
imports: Coq.Arith.EqNat Coq.NArith.BinNat Coq.NArith.Nnat Coq.Init.Byte