proposition: Lemma NumberToString_rec_snd_divmod : forall fuel_n n, n < fuel_n -> exists a, NumberToString_rec fuel_n match snd (NPeano.divmod n 9 0 8) with | 0 => 9 | 1 => 8 | 2 => 7 | 3 => 6 | 4 => 5 | 5 => 4 | 6 => 3 | 7 => 2 | 8 => 1 | S (S (S (S (S (S (S (S (S _)))))))) => 0 end = String a EmptyString.
proof: Proof. destruct fuel_n; intros. omega. destruct (snd (NPeano.divmod n 9 0 8)); [simpl; eauto | ]. do 9 (destruct n0; [simpl; eauto | ]). simpl; eauto. 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