diff options
Diffstat (limited to 'theories/NArith/Ngcd_def.v')
-rw-r--r-- | theories/NArith/Ngcd_def.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/NArith/Ngcd_def.v b/theories/NArith/Ngcd_def.v index fe5185c6b..c25af8717 100644 --- a/theories/NArith/Ngcd_def.v +++ b/theories/NArith/Ngcd_def.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import BinPos BinNat Pgcd. +Require Import BinPos BinNat. Local Open Scope N_scope. @@ -21,7 +21,7 @@ Definition Ngcd (a b : N) := match a, b with | 0, _ => b | _, 0 => a - | Npos p, Npos q => Npos (Pgcd p q) + | Npos p, Npos q => Npos (Pos.gcd p q) end. (** * Generalized Gcd, also computing rests of a and b after @@ -32,7 +32,7 @@ Definition Nggcd (a b : N) := | 0, _ => (b,(0,1)) | _, 0 => (a,(1,0)) | Npos p, Npos q => - let '(g,(aa,bb)) := Pggcd p q in + let '(g,(aa,bb)) := Pos.ggcd p q in (Npos g, (Npos aa, Npos bb)) end. @@ -41,7 +41,7 @@ Definition Nggcd (a b : N) := Lemma Nggcd_gcd : forall a b, fst (Nggcd a b) = Ngcd a b. Proof. intros [ |p] [ |q]; simpl; auto. - generalize (Pggcd_gcd p q). destruct Pggcd as (g,(aa,bb)); simpl; congruence. + generalize (Pos.ggcd_gcd p q). destruct Pos.ggcd as (g,(aa,bb)); simpl; congruence. Qed. (** The other components of Nggcd are indeed the correct factors. *) @@ -53,8 +53,8 @@ Proof. intros [ |p] [ |q]; simpl; auto. now rewrite Pmult_1_r. now rewrite Pmult_1_r. - generalize (Pggcd_correct_divisors p q). - destruct Pggcd as (g,(aa,bb)); simpl. destruct 1; split; congruence. + generalize (Pos.ggcd_correct_divisors p q). + destruct Pos.ggcd as (g,(aa,bb)); simpl. destruct 1; split; congruence. Qed. (** We can use this fact to prove a part of the gcd correctness *) @@ -78,7 +78,7 @@ Proof. intros [ |p] [ |q]; simpl; auto. intros [ |r]. intros (s,H). discriminate. intros ([ |s],Hs) ([ |t],Ht); try discriminate; simpl in *. - destruct (Pgcd_greatest p q r) as (u,H). + destruct (Pos.gcd_greatest p q r) as (u,H). exists s. now inversion Hs. exists t. now inversion Ht. exists (Npos u). simpl; now f_equal. |