equal
deleted
inserted
replaced
525 done |
525 done |
526 |
526 |
527 lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r" |
527 lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r" |
528 apply (simp add: divide_inverse) |
528 apply (simp add: divide_inverse) |
529 apply (case_tac "r=0") |
529 apply (case_tac "r=0") |
530 apply (auto simp add: mult_ac) |
530 apply (auto simp add: ac_simps) |
531 done |
531 done |
532 |
532 |
533 lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u" |
533 lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u" |
534 by (simp add: divide_less_eq) |
534 by (simp add: divide_less_eq) |
535 |
535 |