The Coq mailing list

["Daniel Galvez" <dt.galvez AT gmail.com>]

Hello,

I'm doing a project involving the rationals in the standard library.
I'm trying to convince Coq that:

Qabs (a - b  + c - d) <= Qabs(a - b) + Qabs(c - d).

This should follow easily from the lemma Qabs_triangle in the module
Coq.QArith.Qabs.

However, simply writing the following: fails

Lemma triangle_eq_mult: forall a b c d:Q, Qabs ((a - b) + (c - d)) <= Qabs (a
- b) + Qabs (c -d).
intros.
apply Qabs_triangle.
Abort.

But if I do this:

Qabs ((a - b)  + (c - d)) <= Qabs(a - b) + Qabs(c - d).
intros.
apply Qabs_triangle.
Qed.

Coq is able to do what I want just fine.

Can anyone describe to me how to add parenthese in an expression (such as
turning the first expression into the second expression)? The larger program I
need this statement in makes it such that I cannot simply insert parantheses
manually where I need this proof.

Thank you,
Daniel Galvez