The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

Hello,

I started out trying to prove the following Lemma:
1 <= asr 1000 5 (* arithmetic right shift of 1000 by 5 bits *)

I created to Lemmas which I assume:

Lemma asr_1:
 forall (x: Z),
 x >= 1 -> asr x 1 = x/2.
Admitted.

Lemma asr_2:
 forall (x y z: Z),
 x >= 1 -> asr x (y + z) = asr (asr x y) z.
Admitted.

Now I would like to prove the first Lemma using asr_1 and asr_2. I started out
with:

Lemma test1:
 1 <= asr 1000 5.
Proof.
 apply asr_2 with (x:=1000) (y:=1) (z:=4).
Save.

This, however, gives me the error:
Impossible to unify "asr 1000 (1+4) = asr (asr 1000 1) 4" with "1 <= asr 10000
5)". How can I apply the Lemmas to solve "test1"?

Sincerely,
Michael