diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZBase.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZBase.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 7ad38577f..0c9d006d6 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -56,10 +56,7 @@ Section CentralInduction. Variable A : predicate NZ. -Hypothesis A_wd : predicate_wd NZeq A. - -Add Morphism A with signature NZeq ==> iff as A_morph. -Proof. apply A_wd. Qed. +Hypothesis A_wd : Proper (NZeq==>iff) A. Theorem NZcentral_induction : forall z : NZ, A z -> |