equal
deleted
inserted
replaced
737 |
737 |
738 lemma real_of_nat_zero_iff [iff]: "(real (n::nat) = 0) = (n = 0)" |
738 lemma real_of_nat_zero_iff [iff]: "(real (n::nat) = 0) = (n = 0)" |
739 by (simp add: real_of_nat_def) |
739 by (simp add: real_of_nat_def) |
740 |
740 |
741 lemma real_of_nat_diff: "n \<le> m ==> real (m - n) = real (m::nat) - real n" |
741 lemma real_of_nat_diff: "n \<le> m ==> real (m - n) = real (m::nat) - real n" |
742 by (simp add: add: real_of_nat_def) |
742 by (simp add: add: real_of_nat_def of_nat_diff) |
743 |
743 |
744 lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)" |
744 lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)" |
745 by (simp add: add: real_of_nat_def) |
745 by (simp add: add: real_of_nat_def) |
746 |
746 |
747 lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \<le> 0) = (n = 0)" |
747 lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \<le> 0) = (n = 0)" |