+theorem le_max_n : \forall f: nat \to bool. \forall n:nat.
+max n f \le n.
+intros.elim n.rewrite > max_O_f.apply le_n.
+simplify.elim (f (S n1)).simplify.apply le_n.
+simplify.apply le_S.assumption.
+qed.
+
+theorem le_to_le_max : \forall f: nat \to bool. \forall n,m:nat.
+n\le m \to max n f \le max m f.
+intros.elim H.
+apply le_n.
+apply (trans_le ? (max n1 f)).apply H2.
+cut ((f (S n1) = true \land max (S n1) f = (S n1)) \lor
+(f (S n1) = false \land max (S n1) f = max n1 f)).
+elim Hcut.elim H3.
+rewrite > H5.
+apply le_S.apply le_max_n.
+elim H3.rewrite > H5.apply le_n.
+apply max_S_max.
+qed.
+
+theorem f_m_to_le_max: \forall f: nat \to bool. \forall n,m:nat.
+m\le n \to f m = true \to m \le max n f.
+intros 3.elim n.apply (le_n_O_elim m H).
+apply le_O_n.
+apply (le_n_Sm_elim m n1 H1).
+intro.apply (trans_le ? (max n1 f)).
+apply H.apply le_S_S_to_le.assumption.assumption.
+apply le_to_le_max.apply le_n_Sn.
+intro.simplify.rewrite < H3.
+rewrite > H2.simplify.apply le_n.
+qed.
+
+