proposition: Lemma digitLtBase m {n} : not (m + n < m).
proof: Proof. red; intros; eapply Le.le_Sn_n; eauto using Le.le_trans, Plus.le_plus_l. 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