unknown identifier use

Stream: general

[Yaël Dillies]

Unrelated to your current problem but int.one : ℤ will you need something in ℕ. Rather do use 0 or use 1. Lean will automatically make them naturals.

[Martin Dvořák]

Oh, thanks! That is what I did in the end but didn't know the reason behind it. Thanks for your explanation!