proposition: Lemma opp_spec (x : int) : to_Z (- x)%sint63 = cmod (- to_Z x) wB.
proof: Proof. rewrite to_Z_cmodwB, Uint63.opp_spec. rewrite <- Z.sub_0_l, <- to_Z_mod_Uint63to_Z, Zminus_mod_idemp_r. now rewrite cmod_mod. Qed.
imports: ZArith Uint63 Lia