# Re: [isabelle] Comparing square roots

```Here is one possible approach:

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)"
apply (auto intro!: real_mult_less_mono2)
apply (metis frac_less2 real_mult_commute real_mult_le_cancel_iff2 real_mult_order)
done

The difficult part of this proof for sledgehammer is the inference from k>1 to k>0. Sledgehammer doesn't know anything about arithmetic and has to do everything from first principles.

Larry Paulson

On 12 Aug 2010, at 23:28, John Munroe wrote:

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