proposition: Lemma mul_spec (x y : int) : to_Z (x * y)%sint63 = cmod (to_Z x * to_Z y) wB.
proof: Proof. rewrite to_Z_cmodwB, Uint63.mul_spec. rewrite <- 2!to_Z_mod_Uint63to_Z, <- Zmult_mod by easy. now rewrite cmod_mod. Qed.
imports: ZArith Uint63 Lia