equal
deleted
inserted
replaced
519 lemma nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)" |
519 lemma nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)" |
520 apply (subst zless_int [symmetric]) |
520 apply (subst zless_int [symmetric]) |
521 apply (simp add: order_le_less) |
521 apply (simp add: order_le_less) |
522 apply (case_tac "w < 0") |
522 apply (case_tac "w < 0") |
523 apply (simp add: order_less_imp_le) |
523 apply (simp add: order_less_imp_le) |
524 apply (blast intro: order_less_trans) |
|
525 apply (simp add: linorder_not_less) |
524 apply (simp add: linorder_not_less) |
526 done |
525 done |
527 |
526 |
528 lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)" |
527 lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)" |
529 apply (case_tac "0 < z") |
528 apply (case_tac "0 < z") |