Is ssrnat included in Coq 8.7?

Question

Coq 8.7 integrates the popular Ssreflect library. Its libraries can hence be imported in the following manner:

From Coq Require Import ssreflect ssrfun ssrbool.

However, when I try to import ssrnat it complains that it's Unable to locate library ssrnat with prefix Coq, and I cannot find ssrnat in the Coq distribution on disk either. Was ssrnat deliberately not included for some reason, or folder into another module, or is there just something wrong with my installation?

Answer 1

ssrnat is not included in the main Coq distribution, although some day we hope to provide an extended distribution where more libraries are available by default.

In Coq 8.7, only the tactic language itself ssreflect plus a few basic supporting libraries ssrfun ssrbool were included.

The reason we didn't include more is because ssrnat makes use of the math-comp mathematical hierarchy so this is a more "invasive" change.

Fortunately, thanks to the plugin being included, installing ssrnat is a very easy task.