maintenance request: adapt to coq/coq#17022 #483
Description
Please adapt CompCert to work with rocq-prover/rocq#17022. A suggested strategy is to add Require Btauto to files that Require ZArith and then fix up the cases where auto is now stronger at using hypotheses such as b = true. Other developments have had a handful of cases like this. Thanks!