maintenance request: adapt to coq/coq#17022

[andres-erbsen]

Please adapt CompCert to work with https://github.com/coq/coq/pull/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!