From 65ac316c8bef7b7edd01dd648778de1974a2b3d4 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 7 Mar 2022 14:11:57 +0000
Subject: [PATCH] chore(algebra/order/nonneg): add `nonneg.coe_nat_cast`
 (#12490)

---
 src/algebra/order/nonneg.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/algebra/order/nonneg.lean b/src/algebra/order/nonneg.lean
index a874615d9d093..2123f9d9d14a4 100644
--- a/src/algebra/order/nonneg.lean
+++ b/src/algebra/order/nonneg.lean
@@ -192,6 +192,10 @@ instance linear_ordered_comm_monoid_with_zero [linear_ordered_comm_ring α] :
 def coe_ring_hom [ordered_semiring α] : {x : α // 0 ≤ x} →+* α :=
 ⟨coe, nonneg.coe_one, nonneg.coe_mul, nonneg.coe_zero, nonneg.coe_add⟩
 
+@[simp, norm_cast]
+protected lemma coe_nat_cast [ordered_semiring α] (n : ℕ) : ((↑n : {x : α // 0 ≤ x}) : α) = n :=
+map_nat_cast (coe_ring_hom : {x : α // 0 ≤ x} →+* α) n
+
 instance has_inv [linear_ordered_field α] : has_inv {x : α // 0 ≤ x} :=
 { inv := λ x, ⟨x⁻¹, inv_nonneg.mpr x.2⟩ }