+ generalize in match (H2 (S n1));
+ intro;
+ generalize in match (lt_to_le_to_lt ? ? ? H4 (H5 (le_n ?)));
+ intro;
+ unfold lt in H6;
+ apply le_S_S_to_le;
+ assumption
+ ]
+ | unfold f';
+ simplify;
+ intro;
+ apply (ltb_elim (f (S n1)) (f x1));
+ simplify;
+ intros;
+ [ generalize in match (H2 x1);
+ intro;
+ change in match n1 with (pred (S n1));
+ apply le_to_le_pred;
+ apply H7;
+ apply le_S;
+ assumption
+ | generalize in match (H2 (S n1) (le_n ?));
+ intro;
+ generalize in match (not_lt_to_le ? ? H5);
+ intro;
+ generalize in match (transitive_le ? ? ? H8 H7);
+ intro;
+ cut (f x1 ≠ f (S n1));
+ [ generalize in match (not_eq_to_le_to_lt ? ? Hcut1 H8);
+ intro;
+ unfold lt in H10;
+ generalize in match (transitive_le ? ? ? H10 H7);
+ intro;
+ apply le_S_S_to_le;
+ assumption
+ | unfold Not;
+ intro;
+ generalize in match (H1 ? ? ? ? H10);
+ [ intro;
+ rewrite > H11 in H6;
+ apply (not_le_Sn_n ? H6)
+ | apply le_S;
+ assumption
+ | apply le_n
+ ]
+ ]
+ ]