proposition: Theorem lucas_step_add p p1 p2 z z1 z2 : (2 < Zpos p) -> 0 <= z < 2 ^ (Zpos p) - 1 -> lucas_step p z p1 = z1 -> lucas_step p z1 p2 = z2 -> lucas_step p z (p2 + p1) = z2.
proof: Proof. intros H H0 H1 H2. assert(A1: ZnZ.Specs (op p)). apply cmk_spec; auto. unfold lucas_step. set (o := cmk_op _). set (m := mmake_mod_op _ _ _). assert (F1 : forall z3, 0 <= z3 < ZnZ.to_Z (b p) -> ZnZ.to_Z (znz_of_Z o z3) = z3). intro z3. case z3; simpl. rewrite ZnZ.spec_0; auto. intros p3 [H3 H4]. apply ZnZ.of_pos_correct. apply Z.lt_le_trans with (1 := H4). replace (ZnZ.to_Z (b p)) with (2 ^ Z.pos p - 1). enough (2 ^ Zpos p <= base (ZnZ.digits o)) by auto with zarith. apply Zpower_le_monotone. auto with zarith. assert (F := lucas_f1 H); auto with zarith. rewrite <-(lucas_f2 H); auto. intros p3 [[]]; unfold Z.le; simpl; auto. unfold lucastest_step. rewrite Pos.iter_add; auto. change (@ZnZ.to_Z _ o (lucastest_step o m (lucastest_step o m (znz_of_Z o z) p1) p2) = z2). assert (F : ZnZ.to_Z (lucastest_step o m (znz_of_Z o z) p1) = ZnZ.to_Z (znz_of_Z o z1)). unfold lucas_step in H1; fold o in H1; fold m in H1; rewrite H1. rewrite F1. reflexivity. rewrite <- H1. apply (lucastest_bounded A1 H (lucas_f2 H) (lucas_f3 H)). rewrite F1. rewrite (lucas_f2 H); auto with zarith. replace (ZnZ.to_Z (b p)) with (2 ^ Z.pos p - 1). auto with zarith. rewrite <-(lucas_f2 H); auto with zarith. rewrite lucastest_eq with (p := p) (b := b p) (6 := F); [auto..| | | ]. apply lucas_f2; auto. apply lucas_f3; auto. assert (0 <= ZnZ.to_Z (lucastest_step o m (znz_of_Z o z) p1) < ZnZ.to_Z (b p)). apply (lucastest_bounded A1 H (lucas_f2 H) (lucas_f3 H)). rewrite F1. replace (ZnZ.to_Z (b p)) with (2 ^ Z.pos p - 1). auto with zarith. rewrite <-(lucas_f2 H); auto with zarith. replace (ZnZ.to_Z (b p)) with (2 ^ Z.pos p - 1). auto with zarith. rewrite <-(lucas_f2 H); auto with zarith. auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZCAux W Mod_op LucasLehmer Bits