commit by user mkmluser

[helm.git] / weblib / arithmetics / minimization.ma

diff --git a/weblib/arithmetics/minimization.ma b/weblib/arithmetics/minimization.ma
index eda9d016618d1031be5b126b65b35ca105b9ee11..2959d0f3d1d14eb4b919dff3903d877f7047ce84 100644 (file)
--- a/weblib/arithmetics/minimization.ma
+++ b/weblib/arithmetics/minimization.ma
@@ -23,7 +23,7 @@ let rec max' i f d ≝
       
 definition max ≝ λn.λf.max' n f O.
 
-theorem max_O: ∀f. max O f = O.
+theorem max_O: ∀f. \ 5A href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/A\ 6 O f = O.
 // qed.
 
 theorem max_cases: ∀f.∀n.