Simplified proofs.

src/Flocq_float_prop.v

@@ -159,11 +159,8 @@ Theorem bpow_le_F2R :
   (bpow e <= F2R (Float beta m e))%R.
 Proof.
 intros m e H.
-rewrite <- (Rmult_1_l (bpow e)).
-unfold F2R. simpl.
-apply Rmult_le_compat_r.
-apply bpow_ge_0.
-apply (Z2R_le 1).
+rewrite <- F2R_bpow.
+apply F2R_le_compat.
 now apply (Zlt_le_succ 0).
 Qed.
 
@@ -328,10 +325,7 @@ rewrite <- (Zabs_eq m1), <- abs_F2R.
 apply H1.
 apply Rgt_not_eq.
 apply Rlt_gt.
-unfold F2R. simpl.
-apply Rmult_lt_0_compat.
-now apply (Z2R_lt 0).
-apply bpow_gt_0.
+now apply F2R_gt_0_compat.
 now apply Zlt_le_weak.
 clear H1.
 rewrite abs_F2R, Zabs_eq.

src/Flocq_rnd_FLX.v

@@ -94,8 +94,7 @@ split ; intros H ; rewrite Hx.
 apply generic_format_0.
 exists (Float beta 0 0).
 split.
-unfold F2R. simpl.
-now rewrite Rmult_0_l.
+now rewrite F2R_0.
 apply Zpower_gt_0.
 now apply Zlt_le_trans with (2 := radix_prop beta).
 now apply Zlt_le_weak.
@@ -144,12 +143,11 @@ destruct (Z_eq_dec xm 0) as [H3|H3].
 exists (Float beta 0 0).
 split.
 rewrite H1, H3.
-unfold F2R. simpl.
-now rewrite 2!Rmult_0_l.
+now rewrite 2!F2R_0.
 intros H.
 elim H.
 rewrite H1, H3.
-apply Rmult_0_l.
+apply F2R_0.
 destruct (ln_beta beta (Z2R xm)) as (d,H4).
 specialize (H4 (Z2R_neq _ _ H3)).
 assert (H5: (0 <= prec - d)%Z).

src/Flocq_rnd_generic.v

@@ -28,6 +28,13 @@ Definition generic_format (x : R) :=
   exists f : float beta,
   canonic x f.
 
+Theorem generic_format_0 :
+  generic_format 0.
+Proof.
+exists (Float beta 0 _) ; repeat split.
+now rewrite F2R_0.
+Qed.
+
 Theorem generic_DN_pt_large_pos_ge_pow :
   forall x ex,
   (fexp ex < ex)%Z ->
@@ -109,10 +116,7 @@ rewrite ln_beta_unique with (1 := H) in Hg2.
 simpl in Hg2.
 apply Rlt_not_le with (1 := Hrg).
 rewrite Hg1, Hg2.
-unfold F2R. simpl.
-apply Rmult_le_compat_r.
-apply bpow_ge_0.
-apply Z2R_le.
+apply F2R_le_compat.
 apply Zfloor_lub.
 apply Rmult_le_reg_r with (bpow (fexp ex)).
 apply bpow_gt_0.
@@ -127,12 +131,9 @@ now rewrite <- Hg1.
 (* - positive too small *)
 replace (Zfloor (x * bpow (- fexp ex))) with Z0.
 (* - . rounded *)
-unfold F2R. simpl.
-rewrite Rmult_0_l.
+rewrite F2R_0.
 split.
-exists (Float beta Z0 _) ; repeat split.
-unfold F2R. simpl.
-now rewrite Rmult_0_l.
+exact generic_format_0.
 split.
 apply Rle_trans with (2 := Hx1).
 apply bpow_ge_0.
@@ -158,18 +159,11 @@ apply Rle_lt_trans with (2 := Hx2).
 apply Rle_trans with (2 := Hgx).
 exact (proj1 Hg4).
 rewrite Hg1.
-unfold F2R. simpl.
-pattern (bpow ge) at 1 ; rewrite <- Rmult_1_l.
-apply Rmult_le_compat_r.
-apply bpow_ge_0.
-apply (Z2R_le 1).
+rewrite <- F2R_bpow.
+apply F2R_le_compat.
 apply (Zlt_le_succ 0).
-apply lt_Z2R.
-apply Rmult_lt_reg_r with (bpow ge).
-apply bpow_gt_0.
-rewrite Rmult_0_l.
-unfold F2R in Hg1. simpl in Hg1.
-now rewrite <- Hg1.
+apply F2R_lt_reg with beta ge.
+now rewrite F2R_0, <- Hg1.
 now apply Rlt_le.
 (* - . . *)
 apply sym_eq.
@@ -433,14 +427,6 @@ apply bpow_gt_0.
 exact Hx.
 Qed.
 
-Theorem generic_format_0 :
-  generic_format 0.
-Proof.
-exists (Float beta 0 _) ; repeat split.
-unfold F2R. simpl.
-now rewrite Rmult_0_l.
-Qed.
-
 Theorem canonic_unicity :
   forall x f1 f2,
   canonic x f1 ->
@@ -532,9 +518,7 @@ Theorem generic_DN_pt_small_pos :
 Proof.
 intros x ex Hx He.
 split.
-exists (Float beta 0 _) ; repeat split.
-unfold F2R. simpl.
-now rewrite Rmult_0_l.
+exact generic_format_0.
 split.
 apply Rle_trans with (2 := proj1 Hx).
 apply bpow_ge_0.

src/Flocq_ulp.v

@@ -219,13 +219,11 @@ rewrite Rnd_N_pt_idempotent with (1 := Hxr).
 unfold Rminus.
 rewrite Rplus_opp_r.
 rewrite Rabs_R0.
-unfold ulp, F2R. simpl.
-rewrite Rmult_1_l.
 apply Rmult_le_pos.
 apply Rlt_le.
 apply Rinv_0_lt_compat.
 now apply (Z2R_lt 0 2).
-apply bpow_ge_0.
+now apply F2R_ge_0_compat.
 apply Hd.
 Qed.
 
@@ -237,8 +235,7 @@ Theorem ulp_monotone :
 Proof.
 intros Hm x y Hx Hxy.
 unfold ulp.
-unfold F2R. simpl.
-rewrite 2!Rmult_1_l.
+rewrite 2!F2R_bpow.
 apply -> bpow_le.
 apply Hm.
 now apply ln_beta_monotone.
@@ -249,14 +246,13 @@ Theorem ulp_bpow :
 intros e.
 unfold ulp.
 rewrite (ln_beta_unique beta (bpow e) (e + 1)).
-unfold F2R.
-now rewrite Rmult_1_l.
+apply F2R_bpow.
 rewrite Rabs_pos_eq.
 split.
 apply -> bpow_le.
 omega.
 apply -> bpow_lt.
-omega.
+apply Zlt_succ.
 apply bpow_ge_0.
 Qed.