How to get Subtypes to inherit typeclasses

Stream: new members

[Jem Bishop]

Hi! I want to create a subtype of the natural numbers less than or equal to 5. With
def House := {n : ℕ // n ≤ 5}
this seems to lose all the typeclass instances the natural numbers have, (I can't add or use = with nats) ! How do I get them for this subtype? Thanks!

[Johan Commelin]

@Jem Bishop What is 4 + 4 in this type?

[Johan Commelin]

Note that mathlib has fin 6 and zmod 6 which are two types that have the same definition as House but are equipped with a bunch of typeclass instances.

[Jem Bishop]

I see, thanks for your help!

[Jem Bishop]

In this case I would like 4 + 4 = 5, so I guess I would create these instances for add on fin manually

[Yury G. Kudryashov]

(deleted)