proposition: Lemma phi_p2t63 p : (Zpos p <= 63 -> to_Z (p2t63 p) = Zpos p - 1)%Z.
proof: Proof. intros Hp; unfold p2t63. rewrite phi_sub; rewrite phi1. assert (Z.pos p = to_Z (snd (positive_to_int p))). generalize Hp. rewrite (positive_to_int_spec p). case (fst (positive_to_int p)); auto. intros p1 H; contradict H. rewrite N2Z.inj_pos. apply Zlt_not_le. replace 63%Z with (1 * 63 + 0)%Z; auto with zarith. apply Z.add_lt_le_mono; auto with zarith. 2 : apply phi_nonneg. apply Zmult_lt_compat2; auto with zarith. now compute. rewrite <- H. apply Zmod_small. assert (0 < Zpos p)%Z; auto with zarith. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik