proposition: Lemma pos_mod_spec w p : φ(pos_mod p w) = φ(w) mod (2 ^ φ(p)).
proof: Proof. simpl. unfold pos_mod_int. assert (W:=to_Z_bounded p);assert (W':=to_Z_bounded Uint63.digits);assert (W'' := to_Z_bounded w). case lebP; intros hle. 2: { symmetry; apply Zmod_small. assert (2 ^ φ Uint63.digits < 2 ^ φ p); [ apply Zpower_lt_monotone; auto with zarith | ]. change wB with (2 ^ φ Uint63.digits) in *; auto with zarith. } rewrite <- (shift_unshift_mod_3 φ Uint63.digits φ p φ w) by auto with zarith. replace (φ Uint63.digits - φ p) with (φ (Uint63.digits - p)) by (rewrite sub_spec, Zmod_small; auto with zarith). rewrite lsr_spec, lsl_spec; reflexivity. Qed.
imports: CyclicAxioms ZArith Uint63