The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

Ce n'est pas une preuve evidente, mais le lemme existe dans la
bibliotheque n_Sn : (n:nat)n<>Sn
Apply (n_Sn n); Auto devrait resoudre votre but

Discriminate fonctionne sur une hypothese de la forme 
        c1=c2 
ou c1 et c2 debutent par des constructeurs differents 
ce qui n'est pas votre cas.

En fait si nat n'etait pas le plus petit ensemble clos par O et S,
alors on pourrait construire un terme tel que n=(S n)
La preuve que ce n'est pas possible s'appuie donc sur la structure
inductive de nat.
Pour n=O : O<>S O est resolu par discriminate
puis sion suppose  n<>(S n), on montre (S n)<>(S (S n)) 
en supposant (S n)=(S (S n)) dont on deduit n=(S n) (Tactique
Injection) et finalement une contradiction avec l'hypothese de
recurrence.

Christine Paulin
        
-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  tel : (+33) (0)1 69 15 66 35         fax : (+33) (0)1 69 15 65 86