apply (min_aux_O_f f O).
qed.
theorem min_aux_S : \forall f: nat \to bool. \forall i,n:nat.
(f (n -(S i)) = true \land min_aux (S i) n f = (n - (S i))) \lor
(f (n -(S i)) = false \land min_aux (S i) n f = min_aux i n f).
apply (min_aux_O_f f O).
qed.
theorem min_aux_S : \forall f: nat \to bool. \forall i,n:nat.
(f (n -(S i)) = true \land min_aux (S i) n f = (n - (S i))) \lor
(f (n -(S i)) = false \land min_aux (S i) n f = min_aux i n f).