## Stream: Coq users

### Topic: Simple proof

#### Julin S (Apr 24 2021 at 09:04):

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.
``````

#### Kenji Maillard (Apr 24 2021 at 09:23):

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 ?

#### Théo Winterhalter (Apr 24 2021 at 09:31):

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`.

#### Lessness (Apr 24 2021 at 11:44):

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.

 I'm dumb. One can prove the statement using `lia` already in the beginning.

#### Laurent Théry (Apr 24 2021 at 13:09):

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 : (_ < _ - _).
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: Jan 29 2023 at 01:02 UTC