proposition: Lemma to_Z_succ (x : int) : x <> max_int -> to_Z (succ x) = to_Z x + 1.
proof: Proof. intros neq_x_max. rewrite succ_spec, cmod_small; [> easy |]. assert (to_Z x <> to_Z max_int) by now intros ?; apply neq_x_max, to_Z_inj. rewrite <- to_Z_min; change (wB / 2) with (to_Z max_int + 1). generalize (to_Z_bounded x); lia. Qed.
imports: ZArith Uint63 Lia