equal
deleted
inserted
replaced
760 qed simp |
760 qed simp |
761 from this[of n] \<open>N \<le> n\<close> show "f N = f n" by auto |
761 from this[of n] \<open>N \<le> n\<close> show "f N = f n" by auto |
762 next |
762 next |
763 fix n m :: nat assume "m < n" "n \<le> N" |
763 fix n m :: nat assume "m < n" "n \<le> N" |
764 then show "f m < f n" |
764 then show "f m < f n" |
765 proof (induct rule: less_Suc_induct[consumes 1]) |
765 proof (induct rule: less_Suc_induct) |
766 case (1 i) |
766 case (1 i) |
767 then have "i < N" by simp |
767 then have "i < N" by simp |
768 then have "f i \<noteq> f (Suc i)" |
768 then have "f i \<noteq> f (Suc i)" |
769 unfolding N_def by (rule not_less_Least) |
769 unfolding N_def by (rule not_less_Least) |
770 with \<open>mono f\<close> show ?case by (simp add: mono_iff_le_Suc less_le) |
770 with \<open>mono f\<close> show ?case by (simp add: mono_iff_le_Suc less_le) |