The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Le 10/01/2018 à 07:55, Siddharth Bhat a écrit :
> Thank you, that does help.
> 
> How does the set notation work? I haven't seen that before, that is cool.
> 
> Is there some place that uses Fin in some trivial way? Eg. Establishes a
> bijection with [1..n]? If not, I suppose I can stumble through :)

To establish a bijection between Fin n and { i | i < n }, you are going
to need unicity of proofs for _ < _ which is *not trivial* (at least for
beginners).

le_pirr : forall a b (H1 H2 : a <= b), H1 = H2.
lt_pirr a b (H1 H2 : a < b) : H1 = H2 := le_pirr (S a) b H1 H2.

Good luck ;-)

Dominique