diff options
Diffstat (limited to 'theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v')
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index a169c009d..175b1ad2c 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -408,7 +408,7 @@ Qed. Lemma div2_spec : forall a, div2 a == shiftr a 1. Proof. - intros a. zify. now apply Zdiv2'_spec. + intros a. zify. now apply Zdiv2_spec. Qed. (** Recursion *) |