Library Stdlib.Numbers.Natural.Abstract.NProperties


From Stdlib Require Export NAxioms.
From Stdlib Require Import NMaxMin NParity NPow NSqrt NLog NDiv NDiv0 NGcd NLcm NLcm0 NBits.

The two following functors summarize all known facts about N.
  • NBasicProp provides properties of basic functions: + - * min max <= <
  • NExtraProp provides properties of advanced functions: pow, sqrt, log2, div, gcd, and bitwise functions. NExtraProp0 additionally assumes a / 0 == 0 and a mod 0 == a.
If necessary, the earlier all-in-one functor NProp could be re-obtained via NBasicProp <+ NExtraProp