The Coq mailing list

[Fr�d�ric Gava <frederic.gava AT wanadoo.fr>]

Bonjour,

 

Pour mes demos je suis obliger de démontrer ce petits lemmes:

 

Lemma a_faire: (j:Z) `0<=j<n` ->

`0 <=

      (Cases (Zcompare j `0`) of

           EGAL => `n-1`

       |  _          => `j-1 end) < n`.

 

Bien sur on a l'axiome

 

Axiom good_n:`0<n`.

 

En fait, mon pb est plus général: comment faire passer dans les hypothèses la comparaison et puis faire tous les sous cas...

 

Pour certain je fais des démos par NewInduction. Mais la, je n'y arrive pas...

 

Merci par avance.

 

Frédéric Gava