proposition: Lemma lucas_Zpos p : 2 < Zpos p -> 0 <= 4 < 2 ^ (Zpos p) - 1.
proof: Proof. intros H; split; auto with zarith. assert (8 <= 2 ^Zpos p); auto with zarith. replace 8 with (2 ^ 3); auto with zarith. apply Zpow_facts.Zpower_le_monotone; auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZCAux W Mod_op LucasLehmer Bits