Library Coq.NArith.Ngcd_def

Require Import BinPos BinNat.
Local Open Scope N_scope.

Notation Ndivide := N.divide (only parsing).
Notation Ngcd := N.gcd (only parsing).
Notation Nggcd := N.ggcd (only parsing).
Notation Nggcd_gcd := N.ggcd_gcd (only parsing).
Notation Nggcd_correct_divisors := N.ggcd_correct_divisors (only parsing).
Notation Ngcd_divide_l := N.gcd_divide_l (only parsing).
Notation Ngcd_divide_r := N.gcd_divide_r (only parsing).
Notation Ngcd_greatest := N.gcd_greatest (only parsing).