proposition: Lemma not_digit_when (c : ascii) (x : nat) : (nat_of_ascii c < 48) \/ (57 < nat_of_ascii c) -> unit_digit x <> c.
proof: Proof. assert (mod_fact : x mod 10 < 10). { apply Nat.mod_upper_bound; auto. } intros H e. unfold unit_digit in e. apply (f_equal nat_of_ascii) in e. rewrite nat_ascii_embedding in e. all: lia. Qed.
imports: List Coq.Strings.String Coq.Strings.Ascii Lia Arith QuickChick.Show