# Library Coq.NArith.NArith

Library for binary natural numbers

Require Export BinNums.

Require Export BinPos.

Require Export BinNat.

Require Export Nnat.

Require Export Ndiv_def.

Require Export Nsqrt_def.

Require Export Ngcd_def.

Require Export NArithRing.

N contains an order tactic for natural numbers
Note that N.order is domain-agnostic: it will not prove
1<=2 or x<=x+x, but rather things like x<=y -> y<=x -> x=y.