Search code examples
coq

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.

Solution

  • 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