Library Coq.NArith.Nsqrt_def


Require Import BinNat.

Obsolete file, see BinNat now, only compatibility notations remain here.

Notation Nsqrt_spec := (fun n => N.sqrt_spec n (N.le_0_l n)) (only parsing).