diff options
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 8 |
3 files changed, 11 insertions, 11 deletions
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 2d9eb395a6..3bdbca44a8 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -465,8 +465,8 @@ Section ZModulo. Proof. intros. generalize (Zgcd_is_gcd a b); inversion_clear 1. - destruct H2; destruct H3; clear H4. - assert (H3:=Zgcd_is_pos a b). + destruct H2 as (q,H2); destruct H3 as (q',H3); clear H4. + assert (H4:=Zgcd_is_pos a b). destruct (Z_eq_dec (Zgcd a b) 0). rewrite e; generalize (Zmax_spec a b); omega. assert (0 <= q). @@ -477,7 +477,7 @@ Section ZModulo. generalize (Zmax_spec 0 b) (Zabs_spec b); omega. apply Zle_trans with a. - rewrite H1 at 2. + rewrite H2 at 2. rewrite <- (Zmult_1_l (Zgcd a b)) at 1. apply Zmult_le_compat; auto with zarith. generalize (Zmax_spec a b); omega. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index 44dd2c5934..6facd3c3a6 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -421,22 +421,22 @@ Qed. Lemma gcd_divide_l : forall n m, (gcd n m | n). Proof. - intros n m. apply spec_divide. zify. apply Zgcd_divide_l. + intros n m. apply spec_divide. zify. apply Z.gcd_divide_l. Qed. Lemma gcd_divide_r : forall n m, (gcd n m | m). Proof. - intros n m. apply spec_divide. zify. apply Zgcd_divide_r. + intros n m. apply spec_divide. zify. apply Z.gcd_divide_r. Qed. Lemma gcd_greatest : forall n m p, (p|n) -> (p|m) -> (p|gcd n m). Proof. - intros n m p. rewrite !spec_divide. zify. apply Zgcd_greatest. + intros n m p. rewrite !spec_divide. zify. apply Z.gcd_greatest. Qed. Lemma gcd_nonneg : forall n m, 0 <= gcd n m. Proof. - intros. zify. apply Zgcd_nonneg. + intros. zify. apply Z.gcd_nonneg. Qed. (** Bitwise operations *) diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 33181e32ae..57277b4893 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -347,22 +347,22 @@ Qed. Lemma gcd_divide_l : forall n m, (gcd n m | n). Proof. - intros n m. apply spec_divide. zify. apply Zgcd_divide_l. + intros n m. apply spec_divide. zify. apply Z.gcd_divide_l. Qed. Lemma gcd_divide_r : forall n m, (gcd n m | m). Proof. - intros n m. apply spec_divide. zify. apply Zgcd_divide_r. + intros n m. apply spec_divide. zify. apply Z.gcd_divide_r. Qed. Lemma gcd_greatest : forall n m p, (p|n) -> (p|m) -> (p|gcd n m). Proof. - intros n m p. rewrite !spec_divide. zify. apply Zgcd_greatest. + intros n m p. rewrite !spec_divide. zify. apply Z.gcd_greatest. Qed. Lemma gcd_nonneg : forall n m, 0 <= gcd n m. Proof. - intros. zify. apply Zgcd_nonneg. + intros. zify. apply Z.gcd_nonneg. Qed. (** Bitwise operations *) |