feat: `NNRat.cast`

[YaelDillies]

trafficstars

Define the canonical coercion from the nonnegative rationals to any division semiring.

From LeanAPAP

---

• [x] depends on: #11202
• [x] depends on: #11453
• [ ] depends on: #11480
• [ ] depends on: #11485
• [ ] depends on: #11486
• [ ] depends on: #11499
• [x] depends on: #11503
• [ ] depends on: #11504
• [x] depends on: #11507
• [x] depends on: #11508
• [ ] depends on: #11639