proposition: Theorem mmul_aux2:forall x, x mod (2 ^ Zpos p - 1) = ((x / 2 ^ Zpos p) + (x mod 2 ^ Zpos p)) mod (2 ^ Zpos p - 1).
proof: Proof. intros x; pattern x at 1; rewrite Z_div_mod_eq_full with (b := 2 ^ Zpos p). match goal with |- (?X * ?Y + ?Z) mod (?X - 1) = ?T => replace (X * Y + Z) with (Y * (X - 1) + (Y + Z)); try ring end. rewrite Zplus_mod; auto with zarith. rewrite Z_mod_mult; auto with zarith. rewrite Zplus_0_l. rewrite Zmod_mod; auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux