Library Coq.NArith.Nsqrt_def


Require Import BinNat.

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

Notation Nsqrtrem := N.sqrtrem (compat "8.7").
Notation Nsqrt := N.sqrt (compat "8.7").
Notation Nsqrtrem_spec := N.sqrtrem_spec (compat "8.7").
Notation Nsqrt_spec := (fun n => N.sqrt_spec n (N.le_0_l n)) (only parsing).
Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (compat "8.7").