proposition: Theorem mmul_aux0: Zpos (xO w_digits) - Zpos p1 = Zpos p.
proof: Proof. unfold w_digits. apply trans_equal with (Zpos p + Zpos p1 - Zpos p1). rewrite p_p1; auto with zarith. auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux