equal
deleted
inserted
replaced
446 |
446 |
447 lemma le_trans: "[| i <= j; j <= k |] ==> i <= (k::nat)" |
447 lemma le_trans: "[| i <= j; j <= k |] ==> i <= (k::nat)" |
448 by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans) |
448 by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans) |
449 |
449 |
450 lemma le_anti_sym: "[| m <= n; n <= m |] ==> m = (n::nat)" |
450 lemma le_anti_sym: "[| m <= n; n <= m |] ==> m = (n::nat)" |
451 -- {* @{text order_less_irrefl} could make this proof fail *} |
|
452 by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym) |
451 by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym) |
453 |
452 |
454 lemma Suc_le_mono [iff]: "(Suc n <= Suc m) = (n <= m)" |
453 lemma Suc_le_mono [iff]: "(Suc n <= Suc m) = (n <= m)" |
455 by (simp add: le_simps) |
454 by (simp add: le_simps) |
456 |
455 |