# [isabelle] Comparing square roots

Hi all,
Does anyone know how to prove
lemma "ALL (d1::real) d2 p q1 q2 k. (k > 1 & d1 > 0 & d2 > 0 & p > 0 &
q1 >= q2 & q2 > 0 & d1 < d2) --> k*sqrt(q1*p/d1) > k*sqrt(q2*p/d2)"
?
Even with the lemma:
lemma "ALL (d1::real) d2 p q1 q2. (d1 > 0 & d2 > 0 & p > 0 & q1 >= q2
& q2 > 0 & d1 < d2) --> sqrt(q1*p/d1) > sqrt(q2*p/d2)"
by (simp add: frac_less2 real_mult_order)
I can't seem to make use of it to prove the first. Sledgehammer helped
me prove the second, but it couldn't find anything for the first even
it looks like a rather straightforward extension of the second. Any
help will definitely be useful.
Thanks
John

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*