Elements of Fin when converted to Nat are smaller than the Bound.

[xekoukou]

Are you interested in small proofs like these? I find myself proving things that seem to be of interest to the general public.

[Melvar]

My guess is that it’s the fact that your module is attempting to import itself that’s causing the error.

[jfdm]

Rather than call the module Extra we should probably be consistent with similar purpose modules in base. For example compare the module (and modules under) Data.List.

• https://github.com/idris-lang/Idris-dev/tree/master/libs/base/Data/List
• https://github.com/idris-lang/Idris-dev/tree/master/libs/base/Data/List

[xekoukou]

In the future, I expect proofs like this one to be moved to the main Fin module or somewhere else.
I think that we need a place where to dump proofs that we needed but couldn't find. That is why I put this on contrib so as to be considered experimental.

Then, after a while, someone needs to take the most useful proofs and categorize them.

Keep in mind that ,I think, one can define a minimum set of proofs, called axioms, and not need to pattern match on the Constructors of the Type anymore when proving things. But let us do this in a different time.

[ahmadsalim]

Thanks for the PR!

[ahmadsalim]

@jfdm I just merged it since it was in contrib and if it gets important enough, it would be moved to a better named module anyway.