Library Coq.Numbers.Integer.Abstract.ZProperties

The two following functors summarize all known facts about N.
  • ZBasicProp provides properties of basic functions: + - * min max <= <
  • ZExtraProp provides properties of advanced functions: pow, sqrt, log2, div, gcd, and bitwise functions.
If necessary, the earlier all-in-one functor ZProp could be re-obtained via ZBasicProp <+ ZExtraProp