freescale porting

[helm.git] / helm / software / matita / nlibrary / nat / big_ops.ma

diff --git a/helm/software/matita/nlibrary/nat/big_ops.ma b/helm/software/matita/nlibrary/nat/big_ops.ma
index bda7d7e6b3fa2e8846cc45fec97f022180e34f89..1d2a0e27a12bcae2ffc33a100c3227a8b149d4e3 100644 (file)
--- 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