diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZOrder.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index b11b840928..f76fa94808 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -370,7 +370,7 @@ Qed. safely removed *) Definition NZsucc_iter (n : nat) (m : NZ) := - nat_rec (fun _ => NZ) m (fun _ l => S l) n. + nat_rect (fun _ => NZ) m (fun _ l => S l) n. Theorem NZlt_succ_iter_r : forall (n : nat) (m : NZ), m < NZsucc_iter (Datatypes.S n) m. |