Commit 2022-07-19 18:28 101555b1

refactor(data/real/ennreal): redefine ennreal.to_nnreal in terms of with_top.untop' (#15247)

• redefine ennreal.to_nnreal as with_top.untop' 0;
• use lambda function instead of id for identity coercions of nat and int;
• move with_top.add_monoid_with_one and with_bot.add_monoid_with_one to algebra.order.monoid, add commutative version;
• generalize ennreal.to_nnreal_mul to with_top.