PR !4#34693: feat(Data/Finite/Card): `Nat.card`/`ENat.car...

Stream: triage

[Random Issue Bot]

Today I chose PR #34693 for discussion!

feat(Data/Finite/Card): Nat.card/ENat.card is strictly monotonic on finite sets
Created by @Snir Broshi (@SnirBroshi) on 2026-02-01
Labels: t-data

Is this PR still relevant? Any recent updates? Anyone making progress?

[Snir Broshi]

Reviews appreciated, this is a small PR (+31 −4) which proves that cardinalities are strictly monotonic over finite sets