(* For one of my developments, I need to show show that

(1 + sqrt 2)/(2 * (sqrt (sqrt 2))) < 127/125

But the function sqrt does not compute.  It is only known
through its properties.  Here is how I do it, relying on
a tactic to perform the computations: psatzl R.

sqrt 2 ~ 1.4142...
sqrt (sqrt 2) ~ 1.1892...  so sqrt(sqrt 2) < 1.1893

*)

Require Import Reals Psatz.

Lemma ex_num : (1 + sqrt 2)/(2 * (sqrt (sqrt 2))) < 127/125.
assert (0 < sqrt 2) by (apply sqrt_lt_R0; psatzl R).
assert (0 < sqrt (sqrt 2)) by (apply sqrt_lt_R0; psatzl R).

assert (approx_s2 : sqrt 2 < 14143/10000).
apply Rsqr_incrst_0; try psatzl R.
 rewrite Rsqr_sqrt; unfold Rsqr; psatzl R.

assert (approx_ss2 : 11892/10000 < sqrt (sqrt 2)).
apply Rsqr_incrst_0; try psatzl R; apply Rsqr_incrst_0; try apply Rle_0_sqr.
 repeat rewrite Rsqr_sqrt; unfold Rsqr; psatzl R.

apply Rlt_trans with ((1 + (14143/10000))/(2 * (11892/10000))).
 apply Rmult_le_0_lt_compat; try psatzl R.
  apply Rlt_le, Rinv_0_lt_compat; psatzl R.
 apply Rinv_1_lt_contravar; psatzl R.
psatzl R.
Qed.