diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-11-06 22:46:21 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-11-06 22:46:21 +0000 |
| commit | 81b999ef75c38799b056de9b5dd93b3b6c6ea6d4 (patch) | |
| tree | d04dd3d48c59206b0c3b52448c437519ced8d1d0 /theories/ZArith/Zsqrt.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/Zsqrt.v')
| -rw-r--r-- | theories/ZArith/Zsqrt.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v index 00da766d8..a97750d77 100644 --- a/theories/ZArith/Zsqrt.v +++ b/theories/ZArith/Zsqrt.v @@ -169,7 +169,7 @@ Theorem Zsqrt_plain_is_pos: forall n, 0 <= n -> 0 <= Zsqrt_plain n. Proof. intros n m; case (Zsqrt_interval n); auto with zarith. intros H1 H2; case (Zle_or_lt 0 (Zsqrt_plain n)); auto. - intros H3; absurd_hyp H2; auto; apply Zle_not_lt. + intros H3; contradict H2; auto; apply Zle_not_lt. apply Zle_trans with ( 2 := H1 ). replace ((Zsqrt_plain n + 1) * (Zsqrt_plain n + 1)) with (Zsqrt_plain n * Zsqrt_plain n + (2 * Zsqrt_plain n + 1)); @@ -187,10 +187,10 @@ Proof. intros H1 H2. case (Zle_or_lt a (Zsqrt_plain (a * a))); intros H3; auto. case Zle_lt_or_eq with (1:=H3); auto; clear H3; intros H3. - absurd_hyp H1; auto; apply Zlt_not_le; auto with zarith. + contradict H1; auto; apply Zlt_not_le; auto with zarith. apply Zle_lt_trans with (a * Zsqrt_plain (a * a)); auto with zarith. apply Zmult_lt_compat_r; auto with zarith. - absurd_hyp H2; auto; apply Zle_not_lt; auto with zarith. + contradict H2; auto; apply Zle_not_lt; auto with zarith. apply Zmult_le_compat; auto with zarith. Qed. |