Commit 2024-02-27 17:09 d5525380

fix: correct statement of zpow_ofNat and ofNat_zsmul (#10969) Previously these were syntactically identical to the corresponding zpow_coe_nat and coe_nat_zsmul lemmas, now they are about OfNat.ofNat. Unfortunately, almost every call site uses the ofNat name to refer to Nat.cast, so the downstream proofs had to be adjusted too.