proposition: Lemma to_Z_opp (x : int) : x <> min_int -> to_Z (- x) = - to_Z x.
proof: Proof. intros neq_x_min. rewrite opp_spec, cmod_small; [> easy |]. rewrite <- to_Z_min; change (wB / 2) with (to_Z max_int + 1). pose proof (to_Z_bounded x) as bound. split. - now rewrite Z.opp_le_mono, Z.opp_involutive; transitivity (to_Z max_int). - rewrite Z.opp_lt_mono, Z.opp_involutive. assert (to_Z x <> to_Z min_int) by now intros ?; apply neq_x_min, to_Z_inj. change (- (to_Z max_int + 1)) with (to_Z min_int); lia. Qed.
imports: ZArith Uint63 Lia