proposition: Lemma decimal_thousand : forall n, n < 256 -> (n / 100) mod 10 * 100 + (n / 10) mod 10 * 10 + n mod 10 = n.
proof: Proof. intros. rewrite Nat.div_mod with (y:=10); auto. rewrite Nat.add_cancel_r. replace 100 with (10*10) by auto. rewrite Nat.mul_assoc. rewrite <- Nat.mul_add_distr_r. rewrite Nat.mul_comm. rewrite Nat.mul_cancel_l; auto. rewrite <- Nat.div_div; auto. rewrite (Nat.div_mod (n/10) 10) at 3; auto. rewrite Nat.add_cancel_r. rewrite Nat.mul_comm. rewrite Nat.mul_cancel_l; auto. rewrite Nat.mod_small; auto. rewrite Nat.div_div; auto. simpl. rewrite (Nat.div_lt_upper_bound n 100 9); auto. lia. Qed.
imports: List Coq.Strings.String Coq.Strings.Ascii Lia Arith QuickChick.Show