theorem lt_min_aux_to_false : \forall f:nat \to bool.
\forall n,off,m:nat. n \leq m \to m < (min_aux off n f) \to f m = false.
intros 3.
theorem lt_min_aux_to_false : \forall f:nat \to bool.
\forall n,off,m:nat. n \leq m \to m < (min_aux off n f) \to f m = false.
intros 3.