# How to to use the fact that combining these hypothesis is false in Coq

Suppose that I have a hypothesis H1 : a > y and another hypothesis H2 : a <= y in Coq. I want to use the fact that combining these hypothesis is an instance of False so that I get to prove my goal automatically. How should I do it ? (btw, assume that both a and y are nat).

If you choose to use gt_not_le_stt, you don't need to destruct a nor y.

  Goal forall a y, a > y -> a <= y -> False.
Proof.
intros a y H H0.
apply Arith_prebase.gt_not_le_stt in H.
exact (H H0).
Qed.


Of course, there are a lot of other solutions, depending on the libraries, tactics and lemmas you choose to use (including the magic lia).

There are several quicker solutions.

Require Import PeanoNat.
Lemma helper : forall a y, a > y -> a <= y -> False.
Proof.
intros a y H.
apply Nat.nle_gt. (* Coq guesses the direction of <-> to use *)
exact H. (* conversion between > and < *)
Qed.


For these simple linear inequalities, there is lia.

Require Import Lia.
Lemma helper' : forall a y, a > y -> a <= y -> False.
Proof. lia. Qed.


As mentioned by @Pierre Casteran, there are multiple possible versions. For the record, here is a simple mathcomp-based one.

From mathcomp Require Import all_ssreflect.

Lemma helper : forall a y, a > y -> a <= y -> False.
Proof. by  move=> a y ay; rewrite leqNgt ay. Qed.


whatever .. here's a long-cut...

Lemma helper : forall a y, a > y -> a <= y -> False.
Proof.
intros. destruct y.
- destruct a.
+ apply Arith_prebase.gt_irrefl_stt in H. destruct H.
+ apply Arith_prebase.le_n_0_eq_stt in H0.
rewrite H0 in H. apply Arith_prebase.gt_irrefl_stt in H. destruct H.
- destruct a.
+ apply Arith_prebase.gt_not_le_stt in H. unfold not in H.
apply H in H0. destruct H0.
+ apply Arith_prebase.gt_not_le_stt in H. unfold not in H.
apply H in H0. destruct H0.
Qed.