equal
deleted
inserted
replaced
69 apply (auto simp add: numeral_2_eq_2) |
69 apply (auto simp add: numeral_2_eq_2) |
70 done |
70 done |
71 |
71 |
72 lemma hypreal_inverse_sqrt_pow2: |
72 lemma hypreal_inverse_sqrt_pow2: |
73 "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x" |
73 "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x" |
74 apply (cut_tac n1 = 2 and a1 = "( *f* sqrt) x" in power_inverse [symmetric]) |
74 apply (cut_tac n = 2 and a = "( *f* sqrt) x" in power_inverse [symmetric]) |
75 apply (auto dest: hypreal_sqrt_gt_zero_pow2) |
75 apply (auto dest: hypreal_sqrt_gt_zero_pow2) |
76 done |
76 done |
77 |
77 |
78 lemma hypreal_sqrt_mult_distrib: |
78 lemma hypreal_sqrt_mult_distrib: |
79 "!!x y. [|0 < x; 0 <y |] ==> |
79 "!!x y. [|0 < x; 0 <y |] ==> |