[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.