+theorem f_false_to_le_max: ∀f,n,p. (∃i:nat.i<n∧f i=true) →
+ (∀m. p < m → f m = false) → max n f ≤ p.
+#f #n #p #H1 #H2 @not_lt_to_le % #H3
+@(absurd ?? not_eq_true_false) <(H2 ? H3) @sym_eq
+@(f_max_true ? n H1)
+qed.
+
+theorem exists_forall_lt:∀f,n.
+(∃i. i < n ∧ f i = true) ∨ (∀i. i < n → f i = false).
+#f #n elim n
+ [%2 #i #lti0 @False_ind @(absurd ? lti0) @le_to_not_lt //
+ |#n1 *
+ [* #a * #Ha1 #Ha2 %1 %{a} % // @le_S //
+ |#H cases (true_or_false (f n1)) #HfS >HfS
+ [%1 %{n1} /2/
+ |%2 #i #lei
+ cases (le_to_or_lt_eq ?? lei) #Hi
+ [@H @le_S_S_to_le @Hi | destruct (Hi) //]
+ ]
+ ]
+ ]
+qed.
+
+theorem exists_max_forall_false:∀f,n.
+((∃i. i < n ∧ f i = true) ∧ (f (max n f) = true))∨
+((∀i. i < n → f i = false) ∧ (max n f) = O).
+#f #n
+cases (exists_forall_lt f n)
+ [#H %1 % // @(f_max_true f n) @H
+ |#H %2 % [@H | @max_not_exists @H
+ ]
+qed.
+
+
+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.
+