proposition: Lemma unthree_three_digit (c : ascii) : let n := nat_of_ascii c in unthree_digit (unit_digit (n / 100)) (unit_digit (n / 10)) (unit_digit n) = Some (ascii_of_nat n).
proof: Proof. unfold unthree_digit. do 3 rewrite unit_digit_ascii. rewrite decimal_thousand. auto. apply nat_ascii_bounded. Qed.
imports: List Coq.Strings.String Coq.Strings.Ascii Lia Arith QuickChick.Show