proposition: Lemma unit_digit_ascii : forall n, digit_of_ascii (unit_digit n) = Some (n mod 10).
proof: Proof. intro. assert (mod_fact : n mod 10 < 10). { apply Nat.mod_upper_bound; auto. } unfold unit_digit. unfold digit_of_ascii. rewrite nat_ascii_embedding. replace (48 <=? n mod 10 + 48) with true. replace (n mod 10 + 48 <=? 57) with true. rewrite Nat.add_sub. auto. { symmetry. apply leb_correct. lia. } { symmetry. apply leb_correct. lia. } { lia. } Qed.
imports: List Coq.Strings.String Coq.Strings.Ascii Lia Arith QuickChick.Show