X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fnat%2Fbig_ops.ma;h=1d2a0e27a12bcae2ffc33a100c3227a8b149d4e3;hb=eb4144a401147a44a9620169eb6dafeb8f5a2c17;hp=bda7d7e6b3fa2e8846cc45fec97f022180e34f89;hpb=c6d3537eee27d05490a9555cc7326bc954b356c5;p=helm.git

diff --git a/helm/software/matita/nlibrary/nat/big_ops.ma b/helm/software/matita/nlibrary/nat/big_ops.ma
index bda7d7e6b..1d2a0e27a 100644
--- a/helm/software/matita/nlibrary/nat/big_ops.ma
+++ b/helm/software/matita/nlibrary/nat/big_ops.ma
@@ -22,5 +22,5 @@ nlet rec big_op (M: magma_type) (n: nat) (f: ∀m. lt m n → M) (v: M) on n : M
    [ O ⇒ λ_.v
    | S n' ⇒ λp.op ? (f n' ?) (big_op M n' ? v) ]) (refl ? n).
 ##[ nrewrite > p; napply le_n
-  | #m; #H; napply (f n'); nrewrite > p; napply le_n]
+  | #m; #H; napply (f m); nrewrite > p; napply le_S; nassumption]
 nqed.
\ No newline at end of file