proposition: Lemma p_lt_double_digits : forall n, [|p|] <= Zpos (w_digits << n).
proof: Proof. induction n;simpl. trivial. case (spec_to_Z p); rewrite Pos2Z.inj_xO;auto with zarith. Qed.
imports: ZArith Ndigits Lia BigNumPrelude DoubleType DoubleBase