The Coq mailing list

[Edsko de Vries <Edsko.de.Vries AT cs.tcd.ie>]

Hi,

> and the result in the console is:
>
> 1 subgoal
> x : nat
> y : nat
> H : div2P x y
> ______________________________________(1/1)
> 2 * S y = S (S x)
>
> The thing is that we know that "div2P x y" is true, by the  
> definition we
> made before. I would want to change it for something like:
>
>  x:nat
>  y:nat
> H0:2*y=x \/ 1+2*y=x
>  H:2*y=x
> ===============
> 2*Sy = S(Sx)
>
> That should not be very difficult, because H0 and H are logical  
> deduction of
> the fact that div2P x y is true.

You can unfold the definition of div2P to make it clearer:

unfold div2P in H.

Of course, you cannot simply assume that 2*y = x, you'll need to prove  
your conclusion given either possibiility for the or:

elim H ; intros.

Hope that helps,

Edsko