proposition: Lemma to_lu_succ n : to_lu (N.succ n) = Little.succ (to_lu n).
proof: Proof. destruct n; simpl; trivial. induction p; simpl; rewrite ?IHp; auto using succ_double_alt, double_succ. Qed.
imports: Decimal DecimalFacts PArith NArith