equal
deleted
inserted
replaced
434 apply (simp add: monoseq_def) |
434 apply (simp add: monoseq_def) |
435 apply (auto dest!: le_imp_less_or_eq) |
435 apply (auto dest!: le_imp_less_or_eq) |
436 apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add) |
436 apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add) |
437 apply (induct_tac "ka") |
437 apply (induct_tac "ka") |
438 apply (auto intro: order_trans) |
438 apply (auto intro: order_trans) |
439 apply (erule swap) |
439 apply (erule contrapos_np) |
440 apply (induct_tac "k") |
440 apply (induct_tac "k") |
441 apply (auto intro: order_trans) |
441 apply (auto intro: order_trans) |
442 done |
442 done |
443 |
443 |
444 lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X" |
444 lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X" |