proposition: Theorem zp1_b: [[zp1]] = Zpos p1.
proof: Proof. change ([[DoubleSub.ww_sub w0 wWW w_opp_c w_opp_carry w_sub_c w_opp w_sub w_sub_carry ww_zdigits (WW w0 zp)]] = Zpos p1). rewrite spec_ww_sub. rewrite spec_ww_digits; simpl ww_to_Z. change (w_to_Z w0) with [|w0|]. unfold w0; rewrite ZnZ.spec_0; autorewrite with rm10. change (w_to_Z zp) with [|zp|]. rewrite zp_b. rewrite Zmod_small. rewrite <- p_p1; ring. unfold ww_digits; split. rewrite <- p_p1. assert (0 < Zpos p1); auto with zarith. apply Z.le_lt_trans with (Zpos (xO w_digits)). assert (0 < Zpos p); auto with zarith. unfold base; apply Zpower2_lt_lin; auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux