docs4#Int.ofNat_le

Stream: mathlib4

[Yaël Dillies]

Shouldn't Int.ofNat_le be Int.coe_nat_le? We have docs#Int.coe_nat_nonneg.

[Sky Wilshaw]

I don't think we'd settled on a convention the last time I asked about this, but that was a few weeks ago.

[Sky Wilshaw]

I think I personally prefer the ofNat spelling, because from my perspective coercions are just used to hide function application noise, but if we need to write out the function name anyway, we might as well write its actual name.