proposition: Lemma phi_addmuldiv63 (x y p : int): (to_Z p <= 63)%Z -> (to_Z (addmuldiv p x y) = ((to_Z x * 2 ^ to_Z p + to_Z y / 2 ^ (63 - to_Z p)) mod 2^63))%Z.
proof: Proof. apply addmuldiv_spec. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik