proposition: Lemma to_Z_cmodwB (x : int) : to_Z x = cmod (φ x%uint63) wB.
proof: Proof. unfold to_Z, cmod. case ltbP; change φ (min_int)%uint63 with (wB / 2). - intros ltxmin. rewrite Z.mod_small; [> lia |]. split. + now apply Z.add_nonneg_nonneg; try apply Uint63.to_Z_bounded. + change wB with (wB / 2 + wB / 2) at 2; lia. - rewrite Z.nlt_ge; intros gexmin. rewrite Uint63.opp_spec. rewrite Z_mod_nz_opp_full. + rewrite Z.mod_small by apply Uint63.to_Z_bounded. rewrite <- (Z_mod_plus_full _ (-1)). change (-1 * wB) with (- (wB / 2) - wB / 2). rewrite <- Z.add_assoc, Zplus_minus. rewrite Z.mod_small. * change wB with (wB / 2 + wB / 2) at 1; lia. * split; [> lia |]. apply Z.lt_sub_lt_add_r. transitivity wB; [>| easy]. now apply Uint63.to_Z_bounded. + rewrite Z.mod_small by now apply Uint63.to_Z_bounded. now intros not0; rewrite not0 in gexmin. Qed.
imports: ZArith Uint63 Lia