proposition: Lemma w4_b: [|w4|] = 4 mod [|b|].
proof: Proof. unfold w4; rewrite (add_mod_spec m_op_spec _ _ _ _ w2_b w2_b). rewrite w2_b; rewrite <- Zplus_mod; auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZCAux W Mod_op LucasLehmer Bits