proposition: Lemma cmod_small (x d : Z) : - (d / 2) <= x < d / 2 -> cmod x d = x.
proof: Proof. intros bound. unfold cmod. rewrite Zmod_small; [> lia |]. split; [> lia |]. rewrite Z.lt_add_lt_sub_r. apply (Z.lt_le_trans _ (d / 2)); [> easy |]. now rewrite <- Z.le_add_le_sub_r, Z.add_diag, Z.mul_div_le. Qed.
imports: ZArith Uint63 Lia