CODEWITHSUNDEEP
coq
OrenIshShalom
OrenIshShalom

Reputation: 7162

Coq proof that p<q or p>=q

I'm trying to prove the following trivial lemma:

Lemma lt_or_ge: forall a b : nat,
  ((a <? b) = false) -> (b <= a).
Proof.
  intros a0 b0 H.

I need something like:

((a <? b) = false) -> (a >= b)

But can't seem to find it in Coq libraries. Any help is appreciated, thanks.

Upvotes: 1

Views: 78

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15414

The Search command only takes into account imported modules, meaning you need to you import Arith module to get access to a number of useful (and now searchable) lemmas.

A search query like the following one

From Coq Require Import Arith.
(* queries separated by whitespace mean boolean "and" *)
Search (_ <? _) false (_ <= _).

will get you what you need right away:

lt_or_ge: forall a b : nat, (a <? b) = false -> b <= a
Nat.ltb_ge: forall x y : nat, (x <? y) = false <-> y <= x

Upvotes: 1

Related Questions