diff options
Diffstat (limited to 'theories/ZArith/Zmin.v')
| -rw-r--r-- | theories/ZArith/Zmin.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index 84155d6f2e..98aea6d20f 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -80,8 +80,7 @@ Notation Zmin_plus := Z.add_min_distr_r (only parsing). Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q). Proof. - intros; unfold Zmin, Pmin; simpl; generalize (Pcompare_Eq_eq p q). - destruct Pcompare; auto. + intros; unfold Zmin, Pmin; simpl. destruct Pos.compare; auto. Qed. Lemma Zpos_min_1 : forall p, Zmin 1 (Zpos p) = 1. |