proposition: Lemma NumberToString_rec_lt_10 : forall n m, n > 0 -> m < 10 -> NumberToString_rec n m = NumberToString_rec 1 m.
proof: Proof. simpl; intros. destruct n. - exfalso; eapply Gt.gt_irrefl; eauto. - simpl; destruct (Compare_dec.lt_dec m 10). + reflexivity. + tauto. 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