simplify.assumption.
simplify.
apply (bool_ind (\lambda b:bool.
-(f (S n1) = b) \to (f ([\lambda b:bool.nat] match b in bool with
+(f (S n1) = b) \to (f (match b in bool with
[ true \Rightarrow (S n1)
| false \Rightarrow (max n1 f)])) = true)).
simplify.intro.assumption.
apply (antisym_le a m).assumption.rewrite > (minus_n_O m).assumption.
simplify.
apply (bool_ind (\lambda b:bool.
-(f (m-(S n)) = b) \to (f ([\lambda b:bool.nat] match b in bool with
+(f (m-(S n)) = b) \to (f (match b in bool with
[ true \Rightarrow m-(S n)
| false \Rightarrow (min_aux n m f)])) = true)).
simplify.intro.assumption.
assumption.
qed.
+theorem le_min_aux_r : \forall f:nat \to bool.
+\forall n,off:nat. (min_aux off n f) \le n.
+intros.
+elim off.simplify.rewrite < minus_n_O.
+elim (f n).simplify.apply le_n.
+simplify.apply le_n.
+simplify.elim (f (n -(S n1))).
+simplify.apply le_plus_to_minus.
+rewrite < sym_plus.apply le_plus_n.
+simplify.assumption.
+qed.