Library Coq.Numbers.Natural.Binary.NBinary


Require Import BinPos.
Require Export BinNat.
Require Import NAxioms NProperties.

Local Open Scope N_scope.

BinNat.N already implements NAxiomSig


Module N <: NAxiomsSig := N.