diff options
| author | letouzey | 2007-11-06 22:46:21 +0000 |
|---|---|---|
| committer | letouzey | 2007-11-06 22:46:21 +0000 |
| commit | 81b999ef75c38799b056de9b5dd93b3b6c6ea6d4 (patch) | |
| tree | d04dd3d48c59206b0c3b52448c437519ced8d1d0 /theories/ZArith/Zpow_facts.v | |
| parent | 556df3bfae8a80563f9415199fa8651666eb1932 (diff) | |
small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is
more general.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10295 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zpow_facts.v')
| -rw-r--r-- | theories/ZArith/Zpow_facts.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index 448fa86023..fd8da834d1 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -344,7 +344,7 @@ Theorem rel_prime_Zpower_r: forall i p q, 0 < i -> rel_prime p q -> rel_prime p (q^i). Proof. intros i p q Hi Hpq; generalize Hi; pattern i; apply natlike_ind; auto with zarith; clear i Hi. - intros H; absurd_hyp H; auto with zarith. + intros H; contradict H; auto with zarith. intros i Hi Rec _; rewrite Zpower_Zsucc; auto. apply rel_prime_mult; auto. case Zle_lt_or_eq with (1 := Hi); intros Hi1; subst; auto. @@ -403,7 +403,7 @@ Proof. split; auto with zarith. pattern q1 at 1; replace q1 with (q1 * 1); auto with zarith. apply Zmult_lt_compat_l; auto with zarith. - intros H5; subst; absurd_hyp Hx; auto with zarith. + intros H5; subst; contradict Hx; auto with zarith. apply Zmult_le_0_reg_r with p1; auto with zarith. apply Zdivide_trans with (2 := H); exists p1; auto with zarith. intros r2 Hr2; exists (r2 + r1); subst. |