equal
deleted
inserted
replaced
793 done |
793 done |
794 |
794 |
795 lemma real_of_nat_div2: |
795 lemma real_of_nat_div2: |
796 "0 <= real (n::nat) / real (x) - real (n div x)" |
796 "0 <= real (n::nat) / real (x) - real (n div x)" |
797 apply(case_tac "x = 0") |
797 apply(case_tac "x = 0") |
798 apply simp |
798 apply (simp add: neq0_conv) |
799 apply (simp add: compare_rls) |
799 apply (simp add: neq0_conv compare_rls) |
800 apply (subst real_of_nat_div_aux) |
800 apply (subst real_of_nat_div_aux) |
801 apply assumption |
801 apply assumption |
802 apply simp |
802 apply simp |
803 apply (subst zero_le_divide_iff) |
803 apply (subst zero_le_divide_iff) |
804 apply simp |
804 apply simp |
805 done |
805 done |
806 |
806 |
807 lemma real_of_nat_div3: |
807 lemma real_of_nat_div3: |
808 "real (n::nat) / real (x) - real (n div x) <= 1" |
808 "real (n::nat) / real (x) - real (n div x) <= 1" |
809 apply(case_tac "x = 0") |
809 apply(case_tac "x = 0") |
810 apply simp |
810 apply (simp add: neq0_conv ) |
811 apply (simp add: compare_rls) |
811 apply (simp add: compare_rls neq0_conv ) |
812 apply (subst real_of_nat_div_aux) |
812 apply (subst real_of_nat_div_aux) |
813 apply assumption |
813 apply assumption |
814 apply simp |
814 apply simp |
815 done |
815 done |
816 |
816 |