proposition: Lemma lucasE p : 2 < Zpos p -> lucas_step p 4 (p - 2) = 0 -> lucas p = 0.
proof: Proof. intros H. unfold lucas, lucas_step, lucastest. set (o := cmk_op _). set (m := mmake_mod_op _ _ _). assert (F0 : 1 < ZnZ.to_Z (b p)). replace (ZnZ.to_Z (b p)) with (2 ^ Z.pos p - 1). assert (2 ^ 1 < 2 ^ Z.pos p). apply Zpower_lt_monotone; auto with zarith. replace (2 ^ 1) with 2 in H0; auto with zarith. rewrite <-(lucas_f2 H); auto. assert (F1 : ZnZ.to_Z ZnZ.one = 1). rewrite w1_b with (p := p) (b := b p); [..|auto| ]. rewrite Z.mod_small; auto with zarith. apply cmk_spec; auto. rewrite <-(lucas_f2 H); auto. assert (F2 : ZnZ.to_Z ZnZ.one = 1 mod ZnZ.to_Z (b p)). rewrite Z.mod_small; auto with zarith. intro H1; rewrite <-H1. assert (F3 : ZnZ.to_Z (add_mod m ZnZ.one ZnZ.one) = 2 mod ZnZ.to_Z (b p)). rewrite (add_mod_spec (lucas_f3 H) _ _ 1 1); auto. replace (ZnZ.to_Z ZnZ.one) with 1; auto. apply lucastest_eq with (p := p) (b := b p); [ |auto|..]. apply cmk_spec; auto. apply lucas_f2; auto. apply lucas_f3; auto. rewrite (add_mod_spec (lucas_f3 H) _ _ 2 2); auto. match goal with |- ?X < ?Y => enough (0 <= X < Y) by auto with zarith end. apply Z.mod_pos_bound; auto with zarith. rewrite (add_mod_spec (lucas_f3 H) _ _ 2 2); auto. replace ((ZnZ.to_Z (add_mod m ZnZ.one ZnZ.one))) with (2 mod ZnZ.to_Z (b p)). rewrite <-Z.add_mod. rewrite Z.mod_small. simpl. apply sym_equal. apply (@ZnZ.of_pos_correct _ o). apply cmk_spec; auto. change 4 with (2 ^ 2). apply Zpower_lt_monotone. auto with zarith. split. auto with zarith. assert (F := lucas_f1 H). unfold op in F; simpl in F; unfold o; auto with zarith. split. auto with zarith. change (2 + 2) with (2 ^ 2). replace (ZnZ.to_Z (b p)) with (2 ^ Z.pos p - 1). assert (2 ^ 3 <= 2 ^ Z.pos p). apply Zpower_le_monotone; auto with zarith. change (2 ^ 3) with 8 in H0. change (2 ^ 2) with 4; auto with zarith. rewrite <-(lucas_f2 H); auto. generalize F0. set (u := ZnZ.to_Z _). auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZCAux W Mod_op LucasLehmer Bits