proposition: Lemma nat_of_ascii_small x : Ascii.nat_of_ascii x < 256.
proof: Proof. apply Compare_dec.leb_complete. revert x. intros [[] [] [] [] [] [] [] []]; lazy; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Arith.PeanoNat Coq.Strings.Ascii Coq.Strings.String Fiat.Common.List.Operations Fiat.Common.StringOperations