+
+theorem false_to_lt_max: ∀f,n,m.O < n →
+ f n = false → max m f ≤ n → max m f < n.
+#f #n #m #posn #Hfn #Hmax cases (le_to_or_lt_eq ?? Hmax) -Hmax #Hmax
+ [//
+ |cases (exists_max_forall_false f m)
+ [* #_ #Hfmax @False_ind @(absurd ?? not_eq_true_false) //
+ |* //
+ ]
+ ]
+qed.
+