proposition: Lemma w2_b: [|w2|] = 2 mod [|b|].
proof: Proof. unfold w2; rewrite (add_mod_spec m_op_spec _ _ _ _ w1_b w1_b). rewrite w1_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