| changeset 56536 | aefb4a8da31f |
| parent 56381 | 0556204bc230 |
| child 56889 | 48a745e1bde7 |
--- a/src/HOL/NthRoot.thy Fri Apr 11 12:43:22 2014 +0200 +++ b/src/HOL/NthRoot.thy Fri Apr 11 13:36:57 2014 +0200 @@ -602,7 +602,7 @@ apply (rule_tac b="(a * d - b * c)\<^sup>2" in ord_le_eq_trans) apply (rule zero_le_power2) apply (simp add: power2_diff power_mult_distrib) -apply (simp add: mult_nonneg_nonneg) +apply (simp) apply simp apply (simp add: add_increasing) done