proposition: Lemma NumberToString_rec_10 : forall fuel_m m, 0 < fuel_m -> m < fuel_m -> NumberToString_rec fuel_m m <> "".
proof: Proof. induction fuel_m; simpl; intros. - omega. - destruct (Compare_dec.lt_dec m 10). + destruct m; try (discriminate || omega). destruct m; try (discriminate || omega). destruct m; try (discriminate || omega). destruct m; try (discriminate || omega). destruct m; try (discriminate || omega). destruct m; try (discriminate || omega). destruct m; try (discriminate || omega). destruct m; try (discriminate || omega). destruct m; try (discriminate || omega). destruct m; try (discriminate || omega). + intro H'; apply string_append_nil in H'; intuition. destruct fuel_m. omega. simpl in H2. destruct (snd (NPeano.divmod m 9 0 9)); simpl in *; try discriminate. * destruct (snd (NPeano.divmod m 9 0 9)); simpl in *; try discriminate. destruct n0; simpl in *; try discriminate. destruct n0; simpl in *; try discriminate. destruct n0; simpl in *; try discriminate. destruct n0; simpl in *; try discriminate. destruct n0; simpl in *; try discriminate. destruct n0; simpl in *; try discriminate. destruct n0; simpl in *; try discriminate. destruct n0; simpl in *; try discriminate. destruct n0; simpl in *; try discriminate. destruct n0; simpl in *; try discriminate. destruct n0; simpl in *; try discriminate. destruct n0; simpl in *; try discriminate. destruct n0; simpl in *; try discriminate. destruct n0; simpl in *; try discriminate. destruct n0; simpl in *; try discriminate. destruct n0; simpl in *; try discriminate. 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