equal
deleted
inserted
replaced
434 qed |
434 qed |
435 qed |
435 qed |
436 next |
436 next |
437 show "q \<le> q" |
437 show "q \<le> q" |
438 by (induct q) simp |
438 by (induct q) simp |
439 show "(q < r) = (q \<le> r \<and> q \<noteq> r)" |
439 show "(q < r) = (q \<le> r \<and> \<not> r \<le> q)" |
440 by (simp only: less_rat_def) |
440 by (induct q, induct r) (auto simp add: le_less mult_commute) |
441 show "q \<le> r \<or> r \<le> q" |
441 show "q \<le> r \<or> r \<le> q" |
442 by (induct q, induct r) |
442 by (induct q, induct r) |
443 (simp add: mult_commute, rule linorder_linear) |
443 (simp add: mult_commute, rule linorder_linear) |
444 } |
444 } |
445 qed |
445 qed |