diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Sorting/PermutSetoid.v | 11 | ||||
| -rw-r--r-- | theories/ZArith/Zorder.v | 6 |
2 files changed, 9 insertions, 8 deletions
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v index f1928a1487..fa807c15f8 100644 --- a/theories/Sorting/PermutSetoid.v +++ b/theories/Sorting/PermutSetoid.v @@ -342,8 +342,7 @@ Proof. rewrite if_eqA_refl in H. clear IHl; omega. rewrite IHl; intros. - specialize (H a0); auto with *. - destruct (eqA_dec a a0); simpl; auto with *. + specialize (H a0). omega. Qed. (** Permutation is compatible with InA. *) @@ -394,18 +393,14 @@ Proof. apply permut_length_1. red; red; intros. specialize (P a). simpl in *. - rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto. - (** Bug omega: le "set" suivant ne devrait pas etre necessaire *) - set (u:= if eqA_dec a2 a then 1 else 0) in *; omega. + rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto. omega. right. inversion_clear H0; [|inversion H]. split; auto. apply permut_length_1. red; red; intros. specialize (P a); simpl in *. - rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto. - (** Bug omega: idem *) - set (u:= if eqA_dec b2 a then 1 else 0) in *; omega. + rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto. omega. Qed. (** Permutation is compatible with length. *) diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 32faf5a956..a8cd69bb3c 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -111,6 +111,12 @@ Proof. Z.swap_greater. apply Z.nle_gt. Qed. +Lemma not_Zne n m : ~ Zne n m -> n = m. +Proof. + intros H. + destruct (Z.eq_decidable n m); [assumption|now elim H]. +Qed. + (** * Equivalence and order properties *) (** Reflexivity *) |