The Coq mailing list

[crateo <crateo AT gmail.com>]

Hi, i'm a newbie in all this thing, and i'm struck in this problem. Please,
give me one answer if you can : P. Here we go:

I have this in coq:

Fixpoint div2 (n : nat) : nat :=
  match n with
  |0=> 0
  |S 0=>0
  | S (S p) => S (div2 p)
  end.
Definition div2P (x y : nat) : Prop := 2 * y = x \/ 1 + 2 * y = x.
Require Export ArithRing.
Lemma th : forall x y : nat, div2P x y -> div2P (S (S x )) (S y).
intros.
constructor.

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.


How, for the shake of the glory chicken, can i do that?

Thanks in advance.
-- 
View this message in context: 
http://www.nabble.com/applying-PROP%27s-tp21421615p21421615.html
Sent from the Coq mailing list archive at Nabble.com.