(f (S n1) = b) \to (f ([\lambda b:bool.nat] match b in bool with
[ true \Rightarrow (S n1)
| false \Rightarrow (max n1 f)])) = true) ? ? ?.
-reflexivity.
simplify.intro.assumption.
simplify.intro.apply H.
elim H1.elim H3.generalize in match H5.
split.apply le_S_S_to_le.assumption.assumption.
intros.apply False_ind.apply not_eq_true_false ?.
rewrite < H2.rewrite < H7.rewrite > H6. reflexivity.
+reflexivity.
qed.
theorem lt_max_to_false : \forall f:nat \to bool.
(f (m-(S n)) = b) \to (f ([\lambda b:bool.nat] match b in bool with
[ true \Rightarrow m-(S n)
| false \Rightarrow (min_aux n m f)])) = true) ? ? ?.
-reflexivity.
simplify.intro.assumption.
simplify.intro.apply H.
elim H1.elim H3.elim H4.
absurd f a = false.rewrite < H8.assumption.
rewrite > H5.
apply not_eq_true_false.
+reflexivity.
qed.
theorem lt_min_aux_to_false : \forall f:nat \to bool.
elim H3.
elim le_to_or_lt_eq (n -(S n1)) m.
apply H.apply lt_minus_S_n_to_le_minus_n.assumption.
-rewrite < H6.assumption.assumption.
+rewrite < H6.assumption.
rewrite < H7.assumption.
+assumption.
qed.
theorem le_min_aux : \forall f:nat \to bool.