The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

Hello,

I'm trying to proof an inequality like the following:

Lemma lem1:
forall (x:Z),
(x * 64 / 8 + 1) >= x * 8.

I tried to start changing the term:
change ((x * 8 + 1) >= x * 8).
but I receive the error message "Error: not convertible". It seems to have
something to do with the brackets. If the statement is (x * (64 / 8) ...), I
can easily change the term, and prove it.

My first thought was, it might be because of x being of type Z, so in general,
x * y / z <> x * (y / z), if x * y is not a multiple of z. I then tried 
another
Lemma:

Lemma lem2:
forall (x:Z),
x - 5 + 3 = x - 2.

In this simple example, I could of couse prove it with intuition in a single
step. But even here, "change (x - 2 = x - 2)" fails already.

Why can't I change the terms in those 2 cases?
In general, what is the best approach to simplify more complex inequalities of
such type?

Sincerely,
Michael