diff --git a/examples/Compute.v b/examples/Compute.v
index d44d6be59fbd1ddca4ed32eaf224ac757dd0ea77..88cfdb26cac7e34eb37d14669084ac28b0a939f5 100644
--- a/examples/Compute.v
+++ b/examples/Compute.v
@@ -80,9 +80,8 @@ apply sym_eq, F2R_Zabs.
 Qed.
 
 Definition sqrt (x : float beta) :=
-  let (m, e) := x in
-  if Zlt_bool 0 m then
-    let '(m', e', l) := truncate beta fexp (Fsqrt beta fexp m e) in
+  if Zlt_bool 0 (Fnum x) then
+    let '(m', e', l) := truncate beta fexp (Fsqrt beta fexp x) in
     Float beta (choice false m' l) e'
   else Float beta 0 0.
 
@@ -90,10 +89,10 @@ Theorem sqrt_correct :
   forall x : float beta,
   round beta fexp rnd (R_sqrt.sqrt (F2R x)) = F2R (sqrt x).
 Proof.
-intros [m e].
+intros x.
 unfold sqrt.
 case Zlt_bool_spec ; intros Hm.
-generalize (Fsqrt_correct beta fexp m e Hm).
+generalize (Fsqrt_correct beta fexp x (F2R_gt_0 _ _ Hm)).
 destruct Fsqrt as [[m' e'] l].
 intros [Hs1 Hs2].
 rewrite (round_trunc_sign_any_correct' beta fexp rnd choice rnd_choice _ m' e' l).
@@ -101,7 +100,7 @@ destruct truncate as [[m'' e''] l'].
 now rewrite Rlt_bool_false by apply sqrt_ge_0.
 now rewrite Rabs_pos_eq by apply sqrt_ge_0.
 now left.
-destruct (Req_dec (F2R (Float beta m e)) 0) as [Hz|Hz].
+destruct (Req_dec (F2R x) 0) as [Hz|Hz].
 rewrite Hz, sqrt_0, F2R_0.
 now apply round_0.
 unfold R_sqrt.sqrt.
@@ -159,12 +158,10 @@ now elim Hy0.
 Qed.
 
 Definition div (x y : float beta) :=
-  let (mx, ex) := x in
-  let (my, ey) := y in
-  if Zeq_bool mx 0 then Float beta 0 0
+  if Zeq_bool (Fnum x) 0 then Float beta 0 0
   else
-    let '(m, e, l) := truncate beta fexp (Fdiv beta fexp (Zabs mx) ex (Zabs my) ey) in
-    let s := xorb (Zlt_bool mx 0) (Zlt_bool my 0) in
+    let '(m, e, l) := truncate beta fexp (Fdiv beta fexp (Fabs _ x) (Fabs _ y)) in
+    let s := xorb (Zlt_bool (Fnum x) 0) (Zlt_bool (Fnum y) 0) in
     Float beta (cond_Zopp s (choice s m l)) e.
 
 Theorem div_correct :
@@ -172,41 +169,43 @@ Theorem div_correct :
   F2R y <> 0%R ->
   round beta fexp rnd (F2R x / F2R y) = F2R (div x y).
 Proof.
-intros [mx ex] [my ey] Hy.
+intros x y Hy.
 unfold div.
 case Zeq_bool_spec ; intros Hm.
-rewrite Hm, 2!F2R_0.
-unfold Rdiv.
-rewrite Rmult_0_l.
-now apply round_0.
-assert (Hx: (0 < Zabs mx)%Z) by now apply Z.abs_pos.
-assert (Hy': (0 < Zabs my)%Z).
-  apply Z.abs_pos.
+  destruct x as [mx ex].
+  simpl in Hm.
+  rewrite Hm, 2!F2R_0.
+  unfold Rdiv.
+  rewrite Rmult_0_l.
+  now apply round_0.
+assert (0 < F2R (Fabs _ x))%R as Hx.
+  destruct x as [mx ex].
+  now apply F2R_gt_0, Z.abs_pos.
+assert (0 < F2R (Fabs _ y))%R as Hy'.
+  destruct y as [my ey].
+  apply F2R_gt_0, Z.abs_pos.
   contradict Hy.
   rewrite Hy.
   apply F2R_0.
-generalize (Fdiv_correct beta fexp (Zabs mx) ex (Zabs my) ey Hx Hy').
+generalize (Fdiv_correct beta fexp (Fabs _ x) (Fabs _ y) Hx Hy').
 destruct Fdiv as [[m e] l].
 intros [Hs1 Hs2].
 rewrite (round_trunc_sign_any_correct' beta fexp rnd choice rnd_choice _ m e l).
-destruct truncate as [[m' e'] l'].
-apply (f_equal (fun s => F2R (Float beta (cond_Zopp s (choice s _ _)) _))).
-rewrite Rsgn_div.
-apply f_equal2 ; apply Rsgn_F2R.
-contradict Hm.
-apply eq_0_F2R with (1 := Hm).
-exact Hy.
-unfold Rdiv.
-rewrite Rabs_mult, Rabs_Rinv.
-rewrite <- 2!F2R_Zabs.
-exact Hs2.
-exact Hy.
-left.
-rewrite <- cexp_abs.
-unfold Rdiv.
-rewrite Rabs_mult, Rabs_Rinv.
-now rewrite <- 2!F2R_Zabs.
-exact Hy.
+- destruct truncate as [[m' e'] l'].
+  apply (f_equal (fun s => F2R (Float beta (cond_Zopp s (choice s _ _)) _))).
+  rewrite Rsgn_div.
+  apply f_equal2 ; apply Rsgn_F2R.
+  contradict Hm.
+  apply eq_0_F2R with (1 := Hm).
+  exact Hy.
+- unfold Rdiv.
+  rewrite Rabs_mult, Rabs_Rinv by exact Hy.
+  now rewrite <- 2!F2R_abs.
+- left.
+  rewrite <- cexp_abs.
+  unfold Rdiv.
+  rewrite Rabs_mult, Rabs_Rinv by exact Hy.
+  now rewrite <- 2!F2R_abs.
 Qed.
 
 End Compute.
diff --git a/src/Calc/Div.v b/src/Calc/Div.v
index fa09ef0841d58c08ea2899fc1a7de0af2274cf13..b7a25b660ef9c987d64550a34c3231d2627f6c9d 100644
--- a/src/Calc/Div.v
+++ b/src/Calc/Div.v
@@ -116,20 +116,24 @@ destruct (Z_lt_le_dec 1 m2') as [Hm2''|Hm2''].
   now constructor.
 Qed.
 
-Definition Fdiv m1 e1 m2 e2 :=
+Definition Fdiv (x y : float beta) :=
+  let (m1, e1) := x in
+  let (m2, e2) := y in
   let e' := ((Zdigits beta m1 + e1) - (Zdigits beta m2 + e2))%Z in
   let e := Zmin (Zmin (fexp e') (fexp (e' + 1))) (e1 - e2) in
   let '(m, l) := Fdiv_core m1 e1 m2 e2 e in
   (m, e, l).
 
 Theorem Fdiv_correct :
-  forall m1 e1 m2 e2,
-  (0 < m1)%Z -> (0 < m2)%Z ->
-  let '(m, e, l) := Fdiv m1 e1 m2 e2 in
-  (e <= cexp beta fexp (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)))%Z /\
-  inbetween_float beta m e (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)) l.
+  forall x y,
+  (0 < F2R x)%R -> (0 < F2R y)%R ->
+  let '(m, e, l) := Fdiv x y in
+  (e <= cexp beta fexp (F2R x / F2R y))%Z /\
+  inbetween_float beta m e (F2R x / F2R y) l.
 Proof.
-intros m1 e1 m2 e2 Hm1 Hm2.
+intros [m1 e1] [m2 e2] Hm1 Hm2.
+apply gt_0_F2R in Hm1.
+apply gt_0_F2R in Hm2.
 unfold Fdiv.
 generalize (mag_div_F2R m1 e1 m2 e2 Hm1 Hm2).
 set (e := Zminus _ _).
diff --git a/src/Calc/Sqrt.v b/src/Calc/Sqrt.v
index 39004d24bb12220a6f476a1f0bfb72ee69ce6345..60a9953959221a29d5182053f9713b0e549e0f70 100644
--- a/src/Calc/Sqrt.v
+++ b/src/Calc/Sqrt.v
@@ -164,20 +164,22 @@ now apply IZR_le.
 apply sqrt_ge_0.
 Qed.
 
-Definition Fsqrt m1 e1 :=
+Definition Fsqrt (x : float beta) :=
+  let (m1, e1) := x in
   let e' := (Zdigits beta m1 + e1 + 1)%Z in
   let e := Zmin (fexp (Z.div2 e')) (Z.div2 e1) in
-  let (m, l) := Fsqrt_core m1 e1 e in
+  let '(m, l) := Fsqrt_core m1 e1 e in
   (m, e, l).
 
 Theorem Fsqrt_correct :
-  forall m1 e1,
-  (0 < m1)%Z ->
-  let '(m, e, l) := Fsqrt m1 e1 in
-  (e <= cexp beta fexp (sqrt (F2R (Float beta m1 e1))))%Z /\
-  inbetween_float beta m e (sqrt (F2R (Float beta m1 e1))) l.
+  forall x,
+  (0 < F2R x)%R ->
+  let '(m, e, l) := Fsqrt x in
+  (e <= cexp beta fexp (sqrt (F2R x)))%Z /\
+  inbetween_float beta m e (sqrt (F2R x)) l.
 Proof.
-intros m1 e1 Hm1.
+intros [m1 e1] Hm1.
+apply gt_0_F2R in Hm1.
 unfold Fsqrt.
 set (e := Zmin _ _).
 assert (2 * e <= e1)%Z as He.