Coq доказательство того, что p = q

Question

Я пытаюсь доказать следующую тривиальную лемму:

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

Мне нужно что-то вроде:

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

Но не могу найти его в библиотеках Coq. Любая помощь приветствуется, спасибо.

Answer 1

Команда Search учитывает только импортированные модули, то есть вам нужно импортировать модуль Arith, чтобы получить доступ к ряду полезных (и теперь доступных для поиска) лемм.

Поисковый запрос, подобный следующий

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

сразу даст вам то, что вам нужно:

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