Proving simple inequalities over Nat

Consider the following simple lemma:

Lemma foo : forall (p q r : nat),
    p <> 0 -> p * q < p * r -> q < r.

I would like to prove the above lemma by dividing both sides of the assumed inequality p * q < p * r by p. How could I approach such a proof (assuming that I do not want to prove monotonicity of division and related lemmas by hand)?

The above question is in a fact a rather simple example of a “natural” rewriting method of proving inequalities. Is there a general technique for such statements?

You claim you want to prove this by division, without proving related lemmas by hand, but I don’t think you do. The only reason to do this by hand is for educational purposes, and at that point you might as well prove the monotonicity lemmas by hand. (If you want to find them, you can Require Import Coq.Arith.Arith. Search "<".

If you did want to prove it by division, though, the relevant lemmas that you want are that (a * b) / a = b and d <> 0 -> x < y -> x / d < y / d.

The easy way to prove this lemma is with the non-linear integer arithmetic solver:

Require Import Coq.micromega.Lia.

Lemma foo : forall (p q r : nat),
    p * q < p * r -> q < r.
Proof. intros; nia. Qed.

Note that you don’t need p <> 0, because 0 < 0 is absurd.

1 Like