proposition: Lemma b_pos: 0 < [|b|].
proof: Proof. rewrite b_p. assert (2 ^ 0 < 2 ^ Zpos p). apply Zpower_lt_monotone; auto with zarith. rewrite Zpower_0_r in H; auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZCAux W Mod_op LucasLehmer Bits