proposition: Lemma phi_shiftr63 p n : (to_Z n <= 63)%Z -> to_Z (shiftr63 p n) = (to_Z p / 2 ^ (to_Z n))%Z.
proof: Proof. intro H; unfold shiftr63. case (phi_toZ n); intros Hn1 Hn2. case (phi_toZ p); intros Hp1 Hp2. rewrite phi_addmuldiv63; auto with zarith. 2: rewrite phi_sub; rewrite Zmod_small; rewrite phi63; auto with zarith. rewrite phi0; rewrite Zmult_0_l; rewrite Zplus_0_l. rewrite phi_sub; rewrite phi63. rewrite (Zmod_small (63 - to_Z n)%Z). 2: split; auto with zarith. replace (63 - (63 - to_Z n))%Z with (to_Z n); auto with zarith. apply Z.mod_small; split; auto with zarith. apply Z.div_pos; auto with zarith. case (Zle_lt_or_eq _ _ Hp1); intros HH. 2: rewrite <- HH; rewrite Zdiv_0_l; auto with zarith. apply Z.le_lt_trans with (to_Z p/ 2 ^ 0)%Z; auto with zarith. case (Zle_lt_or_eq _ _ Hn1); intros HH1. 2: rewrite <- HH1; auto with zarith. apply Zdiv_le_compat_l; auto with zarith. split; auto with zarith. apply Zpow_facts.Zpower_lt_monotone; auto with zarith. rewrite Zpow_facts.Zpower_0_r; rewrite Zdiv_1_r; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik