proposition: Lemma NumberToString_rec_inj' : forall fuel_n n m fuel_m, n < fuel_n -> m < fuel_m -> NumberToString_rec fuel_n n = NumberToString_rec fuel_m m -> n = m.
proof: Proof. induction fuel_n. intros; try omega. induction m; auto. destruct n; try omega; intros. destruct fuel_m; try omega. destruct fuel_m; try omega. simpl in H1. destruct (Compare_dec.lt_dec (S n) 10). do 10 (destruct n; try discriminate). omega. omega. symmetry in H1; apply string_append_single in H1; intuition. exfalso. destruct (@NumberToString_rec_snd_divmod fuel_n n); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3). omega. pose proof (divmod_lt_self n); omega. intros. destruct n; simpl in *; try omega. destruct fuel_m; simpl in *; try omega. destruct (Compare_dec.lt_dec (S m) 10); simpl in *. do 10 (destruct m; try discriminate). omega. omega. apply string_append_single in H1; intuition. destruct (@NumberToString_rec_snd_divmod fuel_m m); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3). omega. pose proof (divmod_lt_self m); omega. destruct fuel_m; simpl in *; try omega. destruct (Compare_dec.lt_dec (S n) 10). destruct (Compare_dec.lt_dec (S m) 10). do 9 (destruct n; [ do 9 (try destruct m; try discriminate; try omega; auto) | ]). do 9 (try destruct m; try discriminate; try omega; auto). destruct n. apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_m m); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self m); omega ]. destruct n. apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_m m); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self m); omega ]. destruct n. apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_m m); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self m); omega ]. destruct n. apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_m m); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self m); omega ]. destruct n. apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_m m); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self m); omega ]. destruct n. apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_m m); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self m); omega ]. destruct n. apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_m m); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self m); omega ]. destruct n. apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_m m); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self m); omega ]. destruct n. apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_m m); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self m); omega ]. omega. destruct (Compare_dec.lt_dec (S m) 10). destruct m. symmetry in H1; apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_n n); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self n); omega ]. destruct m. symmetry in H1; apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_n n); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self n); omega ]. destruct m. symmetry in H1; apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_n n); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self n); omega ]. destruct m. symmetry in H1; apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_n n); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self n); omega ]. destruct m. symmetry in H1; apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_n n); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self n); omega ]. destruct m. symmetry in H1; apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_n n); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self n); omega ]. destruct m. symmetry in H1; apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_n n); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self n); omega ]. destruct m. symmetry in H1; apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_n n); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self n); omega ]. destruct m. symmetry in H1; apply string_append_single in H1; intuition; [ exfalso; apply (fun H H' => NumberToString_rec_10 _ _ H H' H3); try omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_n n); [omega | congruence]. exfalso; eapply (fun H H' => NumberToString_rec_10 _ _ H H' H3); [ omega | pose proof (divmod_lt_self n); omega ]. omega. destruct (@NumberToString_rec_snd_divmod fuel_m m); [omega | ]. destruct (@NumberToString_rec_snd_divmod fuel_n n); [omega | ]. rewrite H3, H2 in H1. eapply append_single_char in H1; intuition. eapply IHfuel_n in H4. subst. rewrite <- H2 in H3. eapply IHfuel_n in H3. assert (snd (NPeano.divmod n 9 0 8) = snd (NPeano.divmod m 9 0 8)). revert H3; clear. pose proof (divmod_lt_9 n); pose proof (divmod_lt_9 m); destruct (snd (NPeano.divmod n 9 0 8)); destruct (snd (NPeano.divmod m 9 0 8)); eauto. do 10 (destruct n0; try discriminate; eauto). do 10 (destruct n0; try discriminate; eauto). destruct n0; destruct n1; eauto. do 10 (destruct n1; try discriminate; eauto). do 10 (destruct n0; try discriminate; eauto). destruct n0; destruct n1; eauto. do 10 (destruct n1; try discriminate; eauto). do 10 (destruct n0; try discriminate; eauto). destruct n0; destruct n1; eauto. do 10 (destruct n1; try discriminate; eauto). do 10 (destruct n0; try discriminate; eauto). destruct n0; destruct n1; eauto. do 10 (destruct n1; try discriminate; eauto). do 10 (destruct n0; try discriminate; eauto). destruct n0; destruct n1; eauto. do 10 (destruct n1; try discriminate; eauto). do 10 (destruct n0; try discriminate; eauto). destruct n0; destruct n1; eauto. do 10 (destruct n1; try discriminate; eauto). do 10 (destruct n0; try discriminate; eauto). destruct n0; destruct n1; eauto. do 10 (destruct n1; try discriminate; eauto). do 10 (destruct n0; try discriminate; eauto). destruct n0; destruct n1; eauto. do 10 (destruct n1; try discriminate; eauto). do 10 (destruct n0; try discriminate; eauto). intros; omega. clear H3. rewrite (divmod_eq m n); auto. destruct (NPeano.divmod m 9 0 8); destruct (NPeano.divmod n 9 0 8); simpl in *; congruence. destruct (snd (NPeano.divmod n 9 0 8)); try omega. do 10 (destruct n2; try omega). destruct (snd (NPeano.divmod m 9 0 8)); try omega. do 10 (destruct n2; try omega). pose proof (divmod_lt_self n); omega. pose proof (divmod_lt_self m); omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Numbers.Natural.Peano.NPeano Coq.Strings.String Coq.Arith.Lt Coq.Arith.Compare_dec Coq.Lists.List Coq.ZArith.ZArith