Library Coq.Numbers.Natural.Abstract.NProperties

Require Export NAxioms.
Require Import NMaxMin NParity NPow NSqrt NLog NDiv NGcd NLcm NBits.

Module Type NProp (N:NAxiomsSig) :=
 NMaxMinProp N <+ NParityProp N <+ NPowProp N <+ NSqrtProp N
  <+ NLog2Prop N <+ NDivProp N <+ NGcdProp N <+ NLcmProp N
  <+ NBitsProp N.