I was trying to prove

```
Suppose x>3and y<2. Then x²−2y>5.
```

But couldn't figure how to get with it.

Can you give me some pointers on how to proceed?

I did

```
Theorem simple : forall x y : nat, x > 3 /\ y < 2 -> x*x - 2*y > 5.
Proof.
intros x y H.
destruct H as [H1 H2].
Qed.
```

As a first preliminary step to any formalization, how would you prove it on paper ? What's the main ideas and proof steps that make this statement hold ?

Also—while in this case it seems fine—be wary of subtraction on natural numbers. Since they are natural numbers, they cannot go below zero so `2 - 3`

is in fact `0`

.

For 'unimportant' proof steps you can use `lia`

tactic (after `Require Import Lia.`

).

The hardest step in this proof is to prove that `x*x > 9`

or even `x*x >= 16`

(using assert and induction on `H1: x > 3`

). After that you can use `lia`

to finish proof.

[Edit] I'm dumb. One can prove the statement using `lia`

already in the beginning.

If you want a proof without automation here it is

```
Require Import Arith.
Theorem simple : forall x y : nat, 3 < x /\ y < 2 -> 5 < x*x - 2*y.
Proof.
intros x y [Hx Hy].
Search concl : (_ < _ - _).
apply Nat.lt_add_lt_sub_l.
Search concl : (_ < _ * _).
Search nat "trans".
apply Nat.le_lt_trans with (m := 3 * 3).
Search concl : (_ + _ <= _).
change (3 * 3) with (2 * 2 + 5).
apply plus_le_compat_r.
Search concl : (_ <= _ * _).
apply Nat.mul_le_mono_l.
Search concl : (_ <= _) (_ < _).
apply Nat.lt_le_incl.
trivial.
Search concl : (_ < _ * _).
apply -> Nat.square_lt_mono.
trivial.
Qed.
```

Last updated: Jun 25 2024 at 14:01 UTC