https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/reading.20mathcomp.20book It should be ```coq Coercion nat_of_ord n (i : 'I_n) := let: @Ordinal _ m _ := i in m. ```
https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/reading.20mathcomp.20book
It should be
Coercion nat_of_ord n (i : 'I_n) := let: @Ordinal _ m _ := i in m.