The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

Thank you, the references you gave me helped me to complete the proof. 
However,
it still looks quite complicated:

Lemma test1 :
  1 <= asr 10000 5.
Proof.
change (1 <= asr 10000 (1 + 4)).
rewrite asr_2 with (x:=10000) (y:=1) (z:=4).
rewrite asr_1 with (x:=10000).
change (1 <= asr 5000 (1 + 3)).
rewrite asr_2 with (x:=5000) (y:=1) (z:=3).
rewrite asr_1 with (x:=5000).
change (1 <= asr 2500 (1 + 2)).
rewrite asr_2 with (x:=2500) (y:=1) (z:=2).
rewrite asr_1 with (x:=2500).
change (1 <= asr 1250 (1 + 1)).
rewrite asr_2 with (x:=1250) (y:=1) (z:=1).
rewrite asr_1 with (x:=1250).
change (1 <= asr 625 1).
rewrite asr_1.
change (1 <= 312).
intuition.
intuition.
intuition.
intuition.
intuition.
intuition.
intuition.
intuition.
intuition.
intuition.
Save.

For each step of simplification, I have to manually calculate the values for
[change] and [rewrite], which works of course, but is a lot of work.
- Is there a way to let Coq automatically determine which values for x,y,z 
will match?
- Can I solve all 10 subgoals I have in the end with a single call of 
intuition
at once? I found out how to use [repeat], but it only seems to apply a tactic
multiple times to a single subgoal, not to multiple subgoals at once.