llelf / cocoricoogle Goto Github PK

forall x y : nat, (x <? y) = false <-> y <= x

$ coqtop
Welcome to Coq 8.11.0 (January 2020)

Coq < From Coq Require Import Arith.
[Loading ML file newring_plugin.cmxs ... done]

Coq < Search (forall x y : nat, (x <? y) = false <-> y <= x).
Nat.ltb_ge: forall x y : nat, (x <? y) = false <-> y <= x

$ ./cocoricoogle 'forall x y : nat, (x <? y) = false <-> y <= x'
(* HI.                            *)
(* Loading.                       *)
(* Searching (everything).        *)
(* 10232 entries. 10232 variants. *)

(* THXBYE.                        *)