diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Numbers/Rational/BigQ/QMake.v | 12 | ||||
| -rw-r--r-- | theories/ZArith/Zcompare.v | 9 |
2 files changed, 3 insertions, 18 deletions
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v index d4db2c66d..33267a518 100644 --- a/theories/Numbers/Rational/BigQ/QMake.v +++ b/theories/Numbers/Rational/BigQ/QMake.v @@ -68,15 +68,9 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Proof. intros x; rewrite N.spec_0; generalize (N.spec_pos x). romega. Qed. -(* - Lemma if_fun_commut : forall A B (f:A->B)(b:bool) a a', - f (if b then a else a') = if b then f a else f a'. - Proof. now destruct b. Qed. - - Lemma if_fun_commut' : forall A B C D (f:A->B)(b:{C}+{D}) a a', - f (if b then a else a') = if b then f a else f a'. - Proof. now destruct b. Qed. -*) + + Ltac destr_zcompare := case Z.compare_spec; intros ?H. + Ltac destr_eqb := match goal with | |- context [Z.eqb ?x ?y] => diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v index 49ab619bc..25925a25c 100644 --- a/theories/ZArith/Zcompare.v +++ b/theories/ZArith/Zcompare.v @@ -19,15 +19,6 @@ Local Open Scope Z_scope. (***************************) (** * Comparison on integers *) -Ltac destr_zcompare := - match goal with |- context [Z.compare ?x ?y] => - let H := fresh "H" in - case_eq (Z.compare x y); intro H; - [generalize (Z.compare_eq _ _ H); clear H; intro H | - change (x<y)%Z in H | - change (x>y)%Z in H ] - end. - Lemma Zcompare_Gt_Lt_antisym : forall n m:Z, (n ?= m) = Gt <-> (m ?= n) = Lt. Proof Z.gt_lt_iff. |