The Coq mailing list

[Yevgeniy Makarov <emakarov AT cs.indiana.edu>]

Hello,

I want to prove a simple statement that for any two numbers one of them 
is <= their average. I prove it by contradiction, assuming that both 
numbers x and y are greater than their average, and by adding the 
inequalities I get x + y > x + y. When I am entering this in Coq (moving 
bottom up), I'd like to replace the second x + y by
(avg x y) + (avg x y). How can I do this since the tactics rewrite and 
replace apply to both occurrences?

Thank you,
Yevgeniy