proposition: Theorem lucastest_step_correct: forall p1 z n, 0 <= n -> [|z|] = fst (s n) mod (2 ^ Zpos p - 1) -> [|lucastest_step z p1|] = fst (s (n + Zpos p1)) mod (2 ^ Zpos p - 1).
proof: Proof. unfold lucastest_step. intros p1; pattern p1; apply Pind; simpl iter_pos; simpl s; clear p1. intros z p1 Hp1 H. unfold square_m2. rewrite <- b_p in H. generalize (square_mod_spec m_op_spec _ _ H); intros H1. rewrite (sub_mod_spec m_op_spec _ _ _ _ H1 w2_b). rewrite H1; rewrite w2_b. rewrite H; rewrite <- Zmult_mod. rewrite <- Zminus_mod. rewrite sn by assumption; simpl. rewrite b_p; auto. intros p1 Rec w1 z Hz Hw1. rewrite Pplus_one_succ_l; rewrite iter_pos_plus; simpl iter_pos. match goal with |- context[square_m2 ?X] => set (tmp := X); unfold square_m2; unfold tmp; clear tmp end. generalize (Rec _ _ Hz Hw1); intros H1. rewrite <- b_p in H1. generalize (square_mod_spec m_op_spec _ _ H1); intros H2. rewrite (sub_mod_spec m_op_spec _ _ _ _ H2 w2_b). rewrite H2; rewrite w2_b. rewrite H1; rewrite <- Zmult_mod. rewrite <- Zminus_mod. replace (z + Zpos (1 + p1)) with ((z + Zpos p1) + 1). rewrite sn; simpl fst; try rewrite b_p; auto with zarith. rewrite Zpos_plus_distr; auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZCAux W Mod_op LucasLehmer Bits