-elim off.absurd (le n m).rewrite > minus_n_O.assumption.
-apply lt_to_not_le.rewrite < (min_aux_O_f f n).assumption.
-generalize in match H1.
-elim (min_aux_S f n1 n).
-elim H3.
-absurd (n - S n1 \le m).assumption.
-apply lt_to_not_le.rewrite < H6.assumption.
-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.
-rewrite < H7.assumption.
-assumption.
+generalize in match n; clear n.
+elim off.absurd (le n1 m).assumption.
+apply lt_to_not_le.rewrite < (min_aux_O_f f n1).assumption.
+elim (le_to_or_lt_eq ? ? H1);
+ [ unfold lt in H3;
+ apply (H (S n1));
+ [ assumption
+ | elim (min_aux_S f n n1);
+ [ elim H4;
+ elim (not_le_Sn_n n1);
+ rewrite > H6 in H2;
+ apply (lt_to_le (S n1) n1 ?).
+ apply (le_to_lt_to_lt (S n1) m n1 ? ?);
+ [apply (H3).
+ |apply (H2).
+ ]
+ | elim H4;
+ rewrite < H6;
+ assumption
+ ]
+ ]
+ | rewrite < H3 in H2 ⊢ %.
+ elim (min_aux_S f n n1);
+ [ elim H4;
+ rewrite > H6 in H2;
+ unfold lt in H2;
+ elim (not_le_Sn_n ? H2)
+ | elim H4;
+ assumption
+ ]
+ ]