more tests but failing

robust/weightedmean.v

@@ -471,11 +471,10 @@ End pos_evar.
 (*Notation eps_max := (10 / 126)%mcR.*)
 (*Notation denom := ((3 / 10)^-1)%mcR.*)
 
-Notation eps_max := (100 / 1253)%mcR.
-Notation denom := (3317 / 1000)%mcR.
+(*Notation eps_max := (100 / 1253)%mcR.
+Notation denom := (3317 / 1000)%mcR.*)
 
-(*
-Notation eps_max := (100%:R / 1253%:R)%mcR.
+(*Notation eps_max := (100%:R / 1253%:R)%mcR.
 Notation denom := (3317%:R / 1000%:R)%mcR.
 
 Lemma eps_maxRE : eps_max = (100 / 1253)%coqR.
@@ -486,7 +485,7 @@ Proof.
 by rewrite RdivE; congr (_ / _)%mcR; rewrite /= -INRE INR_IZR_INZ.
 Qed.*)
 
-(*Notation eps_max := (100%:R / 1252%:R)%mcR.
+Notation eps_max := (100%:R / 1252%:R)%mcR.
 Notation denom := (33178%:R / 10000%:R)%mcR.
 
 Lemma eps_maxRE : eps_max = (100 / 1252)%coqR.
@@ -495,7 +494,7 @@ Proof. by rewrite RdivE; congr (_ / _)%mcR; rewrite /= -INRE INR_IZR_INZ. Qed.
 Lemma denomRE : denom = (33178 / 10000)%coqR.
 Proof.
 by rewrite RdivE; congr (_ / _)%mcR; rewrite /= -INRE -common.uint_N_nat INR_IPR.
-Qed.*)
+Qed.
 
 Section invariant.
 Local Open Scope ring_scope.
@@ -898,17 +897,31 @@ rewrite (_ : 2 = 2%coqR); last by rewrite !IZRposE// -!coqRE.
 by rewrite (_ : 4 = 4%coqR)// !IZRposE// -!coqRE.
 Qed.
 
+Lemma from_mcR_to_coqR_manually2 (e : R) :
+  (1 - 3 / 2 * e -
+    (1 - e) *
+    (16^-1 + 2 * e * ((4 * Num.sqrt (2 - e))^-1 + (Num.sqrt (1 - e))^-1) ^+ 2))%mcR =
+  (1 - 3 / 2 * e -
+    (1 - e) *
+    (/16 + 2 * e * (/(4 * sqrt (2 - e)) + (/sqrt (1 - e))) ^ 2))%coqR.
+Proof.
+rewrite !coqRE !RsqrtE'.
+rewrite (_ : 16 = 16%coqR); last by rewrite !IZRposE// -!coqRE.
+rewrite (_ : 2 = 2%coqR); last by rewrite !IZRposE// -!coqRE.
+by rewrite (_ : 4 = 4%coqR)// !IZRposE// -!coqRE.
+Qed.
+
 Lemma bound_evar_ineq_by_interval : bound_evar_ineq eps_max.
 Proof.
 rewrite /bound_evar_ineq/bound_intermediate; apply/RleP.
-(* this works for small constants:*)
+(* this works for small constants:
   rewrite -!coqRE.
   rewrite -!RsqrtE'.
-  interval.
-(* this works for large constants:
+  interval.*)
+(* this works for large constants:*)
 rewrite from_mcR_to_coqR_manually eps_maxRE denomRE.
 rewrite -[in X in (_ <= X)%coqR]coqRE.
-interval.*)
+interval.
 Qed.
 
 (**md ## lemma 1.4, page 5 (part 2) *)
@@ -950,10 +963,11 @@ have ->// :  2 / denom * `V (WP.-RV X) <=
   `V (WP.-RV X).
 rewrite ler_wpM2r // ?variance_ge0' // /bound_intermediate.
 apply/RleP. move: low_eps => /RleP. move: eps0 => /RleP.
-rewrite -!coqRE -!RsqrtE' => ? ?.
-(* doesn't work yet :
+(*rewrite -!coqRE -!RsqrtE' => ? ?.*)
+(* doesn't work yet :*)
+rewrite from_mcR_to_coqR_manually2 denomRE eps_maxRE.
 move=> ? ?.
-rewrite from_mcR_to_coqR_manually denomRE.*)
+rewrite -![in X in (X <= _)%coqR]coqRE.
 interval with (i_prec 20, i_bisect eps).
 Qed.