proposition: Theorem spec_double_size_digits: forall x, Zpos (digits (double_size x)) = 2 * (Zpos (digits x)).
proof: Proof. intros x. rewrite ! digits_level, double_size_level. rewrite 2 digits_dom_op, 2 Pshiftl_nat_Zpower, Nat2Z.inj_succ, Z.pow_succ_r by auto with zarith. ring. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen