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

`Int32`

from the`CompCert.Integers`

module`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.