Reputation: 7162
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
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