Dealing with multiple integer libraries in Coq?

Question

I often get proof terms of the form:

Lemma of_nat_gt_0: forall (n: nat),
(Z.of_nat n >=? Int32.unsigned (Int32.repr 0)) = true.

The theorem is obviously true (Z of a natural will always be >= 0. Similarly, unsigned of a repr of a 0 will yield 0.

However, they are just straight up annoying, because I need to deal with

1. Int32 from the CompCert.Integers module
2. Z.of_nat conversions.

Often, I also have terms from Pos and N definitions.

Thse proofs involve multiple manual rewrites to juggle into some standard form, and then an omega call.

is there some way to "normalize" all of these into a single unified representation?

I understand that this implicitly involves transferring between different rings (eg, Int32 is Z/(2^32 - 1)). It would be nice if there's some way to deal with this, because these are the proofs that get annoyingly long.