The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 29/06/2010 08:52, Sidi a écrit :

> With this definition of div_aux, my question is how can I proof this
> simple lemma :
> 
> Lemma div0 : forall y (H : Acc lt 0), div_aux 0 y H = 0.
> Proof.
> intros.

You have to destruct H, yet it appears in a dependent position in the
goal, so

now dependent inversion H.

Best regards,

Guillaume