proposition: Theorem mmul_aux1: 2 ^ Zpos w_digits = 2 ^ (Zpos w_digits - Zpos p) * 2 ^ Zpos p.
proof: Proof. rewrite <- Zpower_exp; auto with zarith. eq_tac; auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux