feat(data/real/nnreal): use the nonneg instance (#9701)
... to show that `nnreal` forms a conditionally complete linear order with bot.
This requires some fixes in the order hierarchy.
* orders on subtypes are now obtained by lifting `coe` instead of `subtype.val`. This has the nice side benefit that some proofs became simpler.
* `subset_conditionally_complete_linear_order` is now reducible
Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>
Co-authored-by: Johan Commelin <johan@commelin.net>
