proposition: Lemma phi_shiftl63 p n : (to_Z n <= 63)%Z -> (to_Z p * 2 ^ (to_Z n) < 2 ^63)%Z -> (to_Z (shiftl63 p n) = to_Z p * (2 ^ (to_Z n)))%Z.
proof: Proof. intros H H1; unfold shiftl63. case (phi_toZ n); intros Hn1 Hn2. case (phi_toZ p); intros Hp1 Hp2. rewrite phi_addmuldiv63; auto with zarith. rewrite phi0; rewrite Zdiv_0_l; rewrite Zplus_0_r. rewrite Zmod_small; auto with zarith. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik