Library Stdlib.NArith.NArith_base

Library for binary natural numbers

From Stdlib Require Export BinNums.
From Stdlib Require Export BinPos.
From Stdlib Require Export BinNat.
From Stdlib Require Export Nnat.
From Stdlib Require Export Ndiv_def.
From Stdlib Require Export Nsqrt_def.
From Stdlib Require Export Ngcd_def.

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.

Local Open Scope N_scope.

Section TestOrder.
Let test : forall x y, x <=y -> y <=x -> x =y.
End TestOrder.