Recherche:

D'ailleurs TropMDR je me souviens être tombé il y a quelques temps sur une page assez cool liée à Software Foundations, des gens avaient codé une variante de "coqdoc" telle que quand on passe la...

PS : je suis flatté d'entendre dire de mon code Coq "il utilise des techniques avancées, moi je fais avec les outils de base", parce que c'est ce que je passe mon temps à me dire du code *des...

Lemma nth_not_error_impl_In_exists :
forall (b : nat) l, (exists n, nth_error l n = value b) -> In b l.
induction l.
(* Cas nil *)
destruct 1 as [n Hn]. destruct n; discriminate.
(*...

Non, c'est toi qui est obsédé par la constructivité. Si tu veux juste raisonner comme d'habitude sans te prendre la tête, tu ajoutes le tiers exclu, on en a déjà parlé, c'est consistent, c'est prévu...

Le problème ici est un problème de bibliothèques. Les spécifications utilisent d'une part "nth_error" et de l'autre "In", mais évidemment dans la lib standard de Coq il n'y a rien de déjà prêt sur le...