diff options
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/ZArith_dec.v | 14 | ||||
| -rw-r--r-- | theories/ZArith/Zeven.v | 30 |
2 files changed, 22 insertions, 22 deletions
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index a8b5576f54..2dce5fbe4a 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -100,8 +100,8 @@ Section decidability. Definition Z_le_gt_dec : {x <= y} + {x > y}. Proof. - elim Z_le_dec; auto. - intro. right. apply Znot_le_gt; auto. + elim Z_le_dec; auto with arith. + intro. right. apply Znot_le_gt; auto with arith. Defined. Definition Z_gt_le_dec : {x > y} + {x <= y}. @@ -111,17 +111,17 @@ Section decidability. Definition Z_ge_lt_dec : {x >= y} + {x < y}. Proof. - elim Z_ge_dec; auto. - intro. right. apply Znot_ge_lt; auto. + elim Z_ge_dec; auto with arith. + intro. right. apply Znot_ge_lt; auto with arith. Defined. Definition Z_le_lt_eq_dec : x <= y -> {x < y} + {x = y}. Proof. intro H. apply Zcompare_rec with (n := x) (m := y). - intro. right. elim (Zcompare_Eq_iff_eq x y); auto. - intro. left. elim (Zcompare_Eq_iff_eq x y); auto. - intro H1. absurd (x > y); auto. + intro. right. elim (Zcompare_Eq_iff_eq x y); auto with arith. + intro. left. elim (Zcompare_Eq_iff_eq x y); auto with arith. + intro H1. absurd (x > y); auto with arith. Defined. End decidability. diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v index 0c87f62234..4dfce35cec 100644 --- a/theories/ZArith/Zeven.v +++ b/theories/ZArith/Zeven.v @@ -145,32 +145,32 @@ Definition Zdiv2 (z:Z) := Lemma Zeven_div2 : forall n:Z, Zeven n -> n = 2 * Zdiv2 n. Proof. intro x; destruct x. - auto. - destruct p; auto. - intros. absurd (Zeven (Zpos (xI p))); red in |- *; auto. - intros. absurd (Zeven 1); red in |- *; auto. - destruct p; auto. - intros. absurd (Zeven (Zneg (xI p))); red in |- *; auto. - intros. absurd (Zeven (-1)); red in |- *; auto. + auto with arith. + destruct p; auto with arith. + intros. absurd (Zeven (Zpos (xI p))); red in |- *; auto with arith. + intros. absurd (Zeven 1); red in |- *; auto with arith. + destruct p; auto with arith. + intros. absurd (Zeven (Zneg (xI p))); red in |- *; auto with arith. + intros. absurd (Zeven (-1)); red in |- *; auto with arith. Qed. Lemma Zodd_div2 : forall n:Z, n >= 0 -> Zodd n -> n = 2 * Zdiv2 n + 1. Proof. intro x; destruct x. - intros. absurd (Zodd 0); red in |- *; auto. - destruct p; auto. - intros. absurd (Zodd (Zpos (xO p))); red in |- *; auto. - intros. absurd (Zneg p >= 0); red in |- *; auto. + intros. absurd (Zodd 0); red in |- *; auto with arith. + destruct p; auto with arith. + intros. absurd (Zodd (Zpos (xO p))); red in |- *; auto with arith. + intros. absurd (Zneg p >= 0); red in |- *; auto with arith. Qed. Lemma Zodd_div2_neg : forall n:Z, n <= 0 -> Zodd n -> n = 2 * Zdiv2 n - 1. Proof. intro x; destruct x. - intros. absurd (Zodd 0); red in |- *; auto. - intros. absurd (Zneg p >= 0); red in |- *; auto. - destruct p; auto. - intros. absurd (Zodd (Zneg (xO p))); red in |- *; auto. + intros. absurd (Zodd 0); red in |- *; auto with arith. + intros. absurd (Zneg p >= 0); red in |- *; auto with arith. + destruct p; auto with arith. + intros. absurd (Zodd (Zneg (xO p))); red in |- *; auto with arith. Qed. Lemma Z_modulo_2 : |