+definition max_spec \def \lambda f:nat \to bool.\lambda n,m: nat.
+m \le n \land (f m)=true \land (\forall i. m < i \to i \le n \to (f i = false)).
+
+theorem max_spec_to_max: \forall f:nat \to bool.\forall n,m:nat.
+max_spec f n m \to max n f = m.
+intros 2.
+elim n
+ [elim H.elim H1.apply (le_n_O_elim ? H3).
+ apply max_O_f
+ |elim H1.
+ elim (max_S_max f n1)
+ [elim H4.
+ rewrite > H6.
+ apply le_to_le_to_eq
+ [apply not_lt_to_le.
+ unfold Not.intro.
+ apply not_eq_true_false.
+ rewrite < H5.
+ apply H3
+ [assumption|apply le_n]
+ |elim H2.assumption
+ ]
+ |elim H4.
+ rewrite > H6.
+ apply H.
+ elim H2.
+ split
+ [split
+ [elim (le_to_or_lt_eq ? ? H7)
+ [apply le_S_S_to_le.assumption
+ |apply False_ind.
+ apply not_eq_true_false.
+ rewrite < H8.
+ rewrite > H9.
+ assumption
+ ]
+ |assumption
+ ]
+ |intros.
+ apply H3
+ [assumption|apply le_S.assumption]
+ ]
+ ]
+ ]
+qed.
+