We probably want to add multiplication and add better rewrite rules to deal with issues like this: https://github.com/IntersectMBO/cardano-ledger/issues/5138