diff options
Diffstat (limited to 'theories/Structures/GenericMinMax.v')
| -rw-r--r-- | theories/Structures/GenericMinMax.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index ffd0649af..a0ee4caaa 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -440,7 +440,7 @@ Qed. Lemma max_min_antimono f : Proper (eq==>eq) f -> - Proper (le==>inverse le) f -> + Proper (le==>flip le) f -> forall x y, max (f x) (f y) == f (min x y). Proof. intros Eqf Lef x y. @@ -452,7 +452,7 @@ Qed. Lemma min_max_antimono f : Proper (eq==>eq) f -> - Proper (le==>inverse le) f -> + Proper (le==>flip le) f -> forall x y, min (f x) (f y) == f (max x y). Proof. intros Eqf Lef x y. @@ -557,11 +557,11 @@ Module UsualMinMaxLogicalProperties forall x y, min (f x) (f y) = f (min x y). Proof. intros; apply min_mono; auto. congruence. Qed. - Lemma min_max_antimonotone f : Proper (le ==> inverse le) f -> + Lemma min_max_antimonotone f : Proper (le ==> flip le) f -> forall x y, min (f x) (f y) = f (max x y). Proof. intros; apply min_max_antimono; auto. congruence. Qed. - Lemma max_min_antimonotone f : Proper (le ==> inverse le) f -> + Lemma max_min_antimonotone f : Proper (le ==> flip le) f -> forall x y, max (f x) (f y) = f (min x y). Proof. intros; apply max_min_antimono; auto. congruence. Qed. |