proposition: Lemma of_nat_None_iff x : of_nat x = None <-> 255 < x.
proof: Proof. generalize (to_of_nat_option_map x). destruct (of_nat x), (Nat.leb x 255) eqn:H; cbn [option_map]; try congruence. { rewrite PeanoNat.Nat.leb_le in H; split; [ congruence | ]. rewrite PeanoNat.Nat.lt_nge; intro H'; exfalso; apply H'; assumption. } { rewrite PeanoNat.Nat.leb_nle in H; split; [ | reflexivity ]. rewrite PeanoNat.Nat.lt_nge; intro; assumption. } Qed.
imports: Coq.Arith.EqNat Coq.NArith.BinNat Coq.NArith.Nnat Coq.Init.Byte