proposition: Lemma to_Z_abs (x : int) : x <> min_int -> to_Z (abs x) = Z.abs (to_Z x).
proof: Proof. intros neq_x_min. unfold abs; case lebP. - now intros leq_0_x; rewrite Z.abs_eq. - rewrite to_Z_opp by easy. intros nleq_0_x; rewrite Z.abs_neq; [> easy |]. change 0 with (to_Z 0); lia. Qed.
imports: ZArith Uint63 Lia