proposition: Lemma of_lu_double_gen d : of_lu (Little.double d) = N.double (of_lu d) /\ of_lu (Little.succ_double d) = N.succ_double (of_lu d).
proof: Proof. rewrite N.double_spec, N.succ_double_spec. induction d; try destruct IHd as (IH1,IH2); simpl Little.double; simpl Little.succ_double; repeat (simpl_of_lu; rewrite ?IH1, ?IH2); split; reflexivity || ring. Qed.
imports: Decimal DecimalFacts PArith NArith