diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZAddOrder.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAddOrder.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index 917e3fc12..5f68b2bb1 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -350,9 +350,7 @@ Qed. Section PosNeg. Variable P : Z -> Prop. -Hypothesis P_wd : predicate_wd Zeq P. - -Add Morphism P with signature Zeq ==> iff as P_morph. Proof. exact P_wd. Qed. +Hypothesis P_wd : Proper (Zeq ==> iff) P. Theorem Z0_pos_neg : P 0 -> (forall n : Z, 0 < n -> P n /\ P (- n)) -> forall n : Z, P n. |