Commit 3106df88 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merged Rnd_N1 and Rnd_N2 into Rnd_NG.

parent 65368b90
......@@ -96,24 +96,16 @@ Definition Rnd_N_pt (F : R -> Prop) (x f : R) :=
Definition Rnd_N (F : R -> Prop) (rnd : R -> R) :=
forall x : R, Rnd_N_pt F x (rnd x).
Definition Rnd_N1_pt (F : R -> Prop) (P : R -> Prop) (x f : R) :=
Definition Rnd_NG_pt (F : R -> Prop) (P : R -> R -> Prop) (x f : R) :=
Rnd_N_pt F x f /\
( P f \/ forall f2 : R, Rnd_N_pt F x f2 -> f2 = f ).
( P x f \/ forall f2 : R, Rnd_N_pt F x f2 -> f2 = f ).
Definition Rnd_N1 (F : R -> Prop) (P : R -> Prop) (rnd : R -> R) :=
forall x : R, Rnd_N1_pt F P x (rnd x).
Definition Rnd_N2_pt (F : R -> Prop) (P : R -> R -> Prop) (x f : R) :=
Rnd_N_pt F x f /\
forall f2 : R, Rnd_N_pt F x f2 -> P f f2.
Definition Rnd_N2 (F : R -> Prop) (P : R -> R -> Prop) (rnd : R -> R) :=
forall x : R, Rnd_N2_pt F P x (rnd x).
Definition Rnd_NG (F : R -> Prop) (P : R -> R -> Prop) (rnd : R -> R) :=
forall x : R, Rnd_NG_pt F P x (rnd x).
Definition Rnd_NA_pt (F : R -> Prop) (x f : R) :=
Rnd_N_pt F x f /\
forall f2 : R, Rnd_N_pt F x f2 ->
(Rabs f2 <= Rabs f)%R.
forall f2 : R, Rnd_N_pt F x f2 -> (Rabs f2 <= Rabs f)%R.
Definition Rnd_NA (F : R -> Prop) (rnd : R -> R) :=
forall x : R, Rnd_NA_pt F x (rnd x).
......
......@@ -91,11 +91,11 @@ intros Hx'.
apply Hu.
Qed.
Theorem satisfies_any_imp_N2 :
Theorem satisfies_any_imp_NG :
forall (F : R -> Prop) (P : R -> R -> Prop),
satisfies_any F ->
( forall x d u, Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> { P u d } + { P d u } ) ->
{ rnd : R -> R | Rnd_N2 F P rnd }.
( forall x d u, Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> { P x u } + { P x d } ) ->
{ rnd : R -> R | Rnd_NG F P rnd }.
Proof.
intros F P Hany HP.
destruct (satisfies_any_imp_DN F Hany) as (rndd, Hd).
......@@ -216,81 +216,56 @@ now apply Rlt_le.
apply Rle_minus.
now eapply Hd.
(* *** away *)
intros f Hf.
assert (HPr: forall x, F x -> P x x).
clear -HP.
intros x HF.
destruct (HP x x x) as [H|H] ;
repeat split ; trivial ; apply Rle_refl.
destruct (Rnd_N_pt_DN_or_UP_eq F x _ _ f (Hd x) (Hu x) Hf) as [K|K] ; rewrite K.
destruct (total_order_T (Rabs (rndu x - x)) (Rabs (rndd x - x))) as [[H|H]|H].
right.
intros f2 Hxf2.
destruct (Rnd_N_pt_DN_or_UP_eq F x _ _ f2 (Hd x) (Hu x) Hxf2) as [K|K] ; rewrite K.
elim Rlt_not_le with (1 := H).
rewrite <- K.
apply Hf.
eapply Hu.
destruct (HP x _ _ (Hd x) (Hu x)) as [H'|H'].
exact H'.
apply HPr.
eapply Hd.
apply HPr.
eapply Hd.
destruct (total_order_T (Rabs (rndu x - x)) (Rabs (rndd x - x))) as [[H|H]|H].
apply HPr.
eapply Hu.
destruct (HP x _ _ (Hd x) (Hu x)) as [H'|H'].
apply HPr.
apply Hxf2.
eapply Hu.
exact H'.
elim Rgt_not_le with (1 := H).
apply refl_equal.
destruct (HP x (rndd x) (rndu x) (Hd x) (Hu x)) as [H0|H0].
now left.
now left.
right.
intros f2 Hxf2.
destruct (Rnd_N_pt_DN_or_UP_eq F x _ _ f2 (Hd x) (Hu x) Hxf2) as [K|K] ; rewrite K.
apply refl_equal.
elim Rlt_not_le with (1 := H).
rewrite <- K.
apply Hf.
apply Hxf2.
eapply Hd.
Qed.
Theorem satisfies_any_imp_N1 :
forall (F : R -> Prop) (P : R -> Prop),
satisfies_any F ->
( forall x, F x -> P x \/ ~ P x ) ->
( forall x d u, ~ F x -> Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> { P d } + { P u } ) ->
{ rnd : R -> R | Rnd_N1 F P rnd }.
Proof.
intros F P Hany EM HP.
destruct (satisfies_any_imp_N2 F (fun f g => P f \/ g = f) Hany) as (rnd, Hr).
(* . *)
intros x d u Hxd Hxu.
destruct (Req_EM_T d u) as [Hdu|Hdu].
now left ; right.
destruct (HP x d u) as [H|H] ; trivial.
intros HF.
apply Hdu.
apply trans_eq with x.
now apply Rnd_DN_pt_idempotent with F.
apply sym_eq.
now apply Rnd_UP_pt_idempotent with F.
now right ; left.
now left ; left.
(* . *)
exists rnd.
intros x.
apply <- Rnd_N1_N2_pt.
apply (Hr x).
intros f g Hf Hg.
apply iff_refl.
exact EM.
Qed.
Theorem satisfies_any_imp_NA :
forall F : R -> Prop,
satisfies_any F ->
{ rnd : R -> R | Rnd_NA F rnd }.
Proof.
intros F Hany.
apply (satisfies_any_imp_N2 F (fun a b => (Rabs b <= Rabs a)%R) Hany).
destruct (satisfies_any_imp_NG F (fun a b => (Rabs a <= Rabs b)%R) Hany) as (rnd, Hrnd).
intros x d u Hxd Hxu.
destruct (Rle_lt_dec (Rabs d) (Rabs u)) as [H|H].
now left.
destruct (Rle_lt_dec 0 x) as [Hx|Hx].
left.
rewrite Rabs_pos_eq with (1 := Hx).
rewrite Rabs_pos_eq.
apply Hxu.
apply Rle_trans with (1 := Hx).
apply Hxu.
right.
now apply Rlt_le.
rewrite Rabs_left with (1 := Hx).
rewrite Rabs_left1.
apply Ropp_le_contravar.
apply Hxd.
apply Rlt_le.
apply Rle_lt_trans with (2 := Hx).
apply Hxd.
exists rnd.
intros x.
apply <- Rnd_NA_NG_pt.
apply Hrnd.
apply Hany.
Qed.
End RND_ex.
......@@ -24,12 +24,12 @@ Variable prop_exp : valid_exp fexp.
Notation format := (generic_format beta fexp).
Notation canonic := (canonic beta fexp).
Definition Rnd_gNE_pt (x f : R) :=
Rnd_N_pt format x f /\
( ( exists g : float beta, canonic f g /\ Zeven (Fnum g) /\
forall f2 : R, forall g : float beta, Rnd_N_pt format x f2 ->
canonic f2 g -> Zeven (Fnum g) -> (Rabs f2 <= Rabs f)%R ) \/
( forall f2 : R, Rnd_N_pt format x f2 -> f = f2 ) ).
Definition gNE_prop x f :=
exists g : float beta, canonic f g /\ Zeven (Fnum g) /\
forall f2 : R, forall g2 : float beta, Rnd_N_pt format x f2 ->
canonic f2 g2 -> Zeven (Fnum g2) -> (Rabs f2 <= Rabs f)%R.
Definition Rnd_gNE_pt := Rnd_NG_pt format gNE_prop.
Definition Rnd_gNE (rnd : R -> R) :=
forall x : R, Rnd_gNE_pt x (rnd x).
......@@ -38,42 +38,26 @@ Theorem Rnd_gNE_pt_sym :
forall x f : R,
Rnd_gNE_pt (-x) (-f) -> Rnd_gNE_pt x f.
Proof.
intros x f (H1,H2).
split.
apply Rnd_N_pt_sym.
apply Rnd_NG_pt_sym.
apply generic_format_sym.
exact H1.
(* . *)
destruct H2 as [((m,e),((H2,H3),H4))|H2].
left.
clear. unfold gNE_prop.
intros x f ((m, e), (Hfg, (Hg, H))).
exists (Float beta (-m) e).
repeat split.
now rewrite <- opp_F2R, <- H2, Ropp_involutive.
simpl in H3 |- *.
now rewrite <- ln_beta_opp.
simpl in H4 |- *.
split.
now apply canonic_sym.
split.
rewrite Zopp_eq_mult_neg_1.
now apply Zeven_mult_Zeven_l.
intros f2 g Hx Hxg Hg.
rewrite <- (Rabs_Ropp f), <- (Rabs_Ropp f2).
eapply H4.
intros f2 g2 Hf2 Hfg2 Hg2.
rewrite Rabs_Ropp, <- (Rabs_Ropp f2).
apply H with (Float beta (-Fnum g2) (Fexp g2)).
apply Rnd_N_pt_sym.
apply generic_format_sym.
now rewrite 2!Ropp_involutive.
eapply canonic_sym.
eexact Hxg.
simpl.
now rewrite Ropp_involutive.
apply canonic_sym.
exact Hfg2.
rewrite Zopp_eq_mult_neg_1.
now apply Zeven_mult_Zeven_l.
(* . *)
right.
intros f2 H3.
rewrite <- (Ropp_involutive f), <- (Ropp_involutive f2).
apply f_equal.
apply H2.
apply Rnd_N_pt_sym.
apply generic_format_sym.
now rewrite 2!Ropp_involutive.
Qed.
Lemma canonic_imp_Fnum :
......@@ -124,49 +108,54 @@ apply -> epow_le.
now apply Zlt_le_weak.
Qed.
Theorem Rnd_gNE_pt_unicity :
forall x f1 f2 : R,
Rnd_gNE_pt x f1 -> Rnd_gNE_pt x f2 ->
f1 = f2.
Lemma Rnd_gNE_pt_unicity_prop :
Rnd_NG_pt_unicity_prop format gNE_prop.
Proof.
intros x f1 f2 (H1,[Hf1|Hf1]) (H2,Hf2).
destruct Hf2 as [Hf2|Hf2].
intros x d u Hxd1 Hxd2 Hxu1 Hxu2 Hd Hu.
assert (H: Rabs d = Rabs u).
(* . *)
destruct Hf1 as (g1, (Hg1a, (Hg1b, Hg1c))).
destruct Hf2 as (g2, (Hg2a, (Hg2b, Hg2c))).
assert (Rabs f1 = Rabs f2).
destruct Hd as (gd, Hd).
destruct Hu as (gu, Hu).
apply Rle_antisym.
now apply Hg2c with g1.
now apply Hg1c with g2.
now apply Hu with gd.
now apply Hd with gu.
destruct (Rle_or_lt 0 x) as [Hx|Hx].
rewrite (Rabs_pos_eq f1) in H.
(* . *)
rewrite (Rabs_pos_eq d) in H.
rewrite H.
apply Rabs_pos_eq.
apply Rnd_N_pt_pos with format x.
apply generic_format_0.
exact Hx.
exact H2.
exact Hxu2.
apply Rnd_N_pt_pos with format x.
apply generic_format_0.
exact Hx.
exact H1.
rewrite (Rabs_left1 f1) in H.
rewrite <- (Ropp_involutive f1), <- (Ropp_involutive f2).
rewrite H.
exact Hxd2.
(* . *)
rewrite (Rabs_left1 u) in H.
rewrite <- (Ropp_involutive d), <- (Ropp_involutive u).
apply sym_eq.
apply f_equal.
rewrite <- H.
apply Rabs_left1.
apply Rnd_N_pt_neg with format x.
apply generic_format_0.
now apply Rlt_le.
exact H2.
exact Hxd2.
apply Rnd_N_pt_neg with format x.
apply generic_format_0.
now apply Rlt_le.
exact H1.
(* . *)
apply sym_eq.
now apply Hf2.
now apply Hf1.
exact Hxu2.
Qed.
Theorem Rnd_gNE_pt_unicity :
forall x f1 f2 : R,
Rnd_gNE_pt x f1 -> Rnd_gNE_pt x f2 ->
f1 = f2.
Proof.
apply Rnd_NG_pt_unicity.
apply Rnd_gNE_pt_unicity_prop.
Qed.
Theorem Rnd_gNE_pt_monotone :
......@@ -174,13 +163,8 @@ Theorem Rnd_gNE_pt_monotone :
Rnd_gNE_pt x f -> Rnd_gNE_pt y g ->
(x <= y)%R -> (f <= g)%R.
Proof.
intros x y f g (Hx1,Hx2) (Hy1,Hy2) [Hxy|Hxy].
eapply Rnd_N_pt_monotone ; eassumption.
apply Req_le.
apply Rnd_gNE_pt_unicity with x.
now split.
rewrite Hxy.
now split.
apply Rnd_NG_pt_monotone.
apply Rnd_gNE_pt_unicity_prop.
Qed.
Theorem Rnd_gNE_pt_idempotent :
......@@ -193,10 +177,11 @@ destruct Hxf as (Hxf1,_).
now apply Rnd_N_pt_idempotent with format.
Qed.
Definition Rnd_NE_pt (x f : R) :=
Rnd_N_pt format x f /\
( ( exists g : float beta, canonic f g /\ Zeven (Fnum g) ) \/
( forall f2 : R, Rnd_N_pt format x f2 -> f = f2 ) ).
Definition NE_prop (_ : R) f :=
exists g : float beta, canonic f g /\ Zeven (Fnum g).
Definition Rnd_NE_pt :=
Rnd_NG_pt format NE_prop.
Definition DN_UP_parity_pos_prop :=
forall x xd xu cd cu,
......@@ -261,10 +246,9 @@ Qed.
Theorem Rnd_NE_pt_aux :
DN_UP_parity_prop ->
forall x f,
format f ->
( Rnd_gNE_pt x f <-> Rnd_NE_pt x f ).
Proof.
intros HP x f Hf.
intros HP x f.
split.
(* . *)
intros (H1, [H2|H2]).
......@@ -349,13 +333,10 @@ Qed.
Theorem Rnd_NE_pt_FIX :
forall x f,
FIX_format beta emin f ->
( Rnd_gNE_pt FIXf x f <-> Rnd_NE_pt FIXf x f ).
Proof.
intros x f Hf.
apply Rnd_NE_pt_aux.
exact DN_UP_parity_FIX.
now apply -> FIX_format_generic.
Qed.
End Flocq_rnd_NE_FIX.
......@@ -530,14 +511,11 @@ Qed.
Theorem Rnd_NE_pt_FLX :
forall x f,
FLX_format beta prec f ->
( Rnd_gNE_pt FLXf x f <-> Rnd_NE_pt FLXf x f ).
Proof.
intros x f Hf.
apply Rnd_NE_pt_aux.
apply DN_UP_parity_aux.
exact DN_UP_parity_FLX_pos.
now apply -> FLX_format_generic.
Qed.
End Flocq_rnd_NE_FLX.
......@@ -592,7 +570,42 @@ now apply Rlt_le.
apply canonic_fun_eq with (2 := Hd).
apply sym_eq.
apply FIX_FLT_exp_subnormal.
admit.
intros Hxd0.
apply Zeven_not_Zodd with (1 := Heu).
rewrite canonic_unicity with (f2 := Float beta 1 emin) (1 := Hu).
exact (Zodd_2p_plus_1 0).
assert (H: xu = bpow emin).
rewrite (ulp_pred_succ_pt beta FLTf (FLT_exp_correct emin prec Hp) x xd xu Hfx Hxd Hxu).
rewrite Hxd0, Rplus_0_l.
unfold ulp, F2R. simpl.
rewrite Rmult_1_l.
apply f_equal.
unfold FLT_exp.
apply Zmax_right.
destruct (ln_beta beta x) as (ex, Hex).
simpl.
cut (ex - 1 <= emin + prec - 1)%Z. omega.
apply <- epow_le.
apply Rle_trans with (2 := Hx).
rewrite <- (Rabs_pos_eq _ (Rlt_le _ _ Hx0)).
apply Hex.
now apply Rgt_not_eq.
rewrite H.
split.
apply sym_eq.
apply Rmult_1_l.
unfold FLT_exp.
rewrite ln_beta_unique with beta (bpow emin) (emin + 1)%Z.
apply sym_eq.
apply Zmax_right.
simpl. omega.
rewrite Rabs_pos_eq.
split.
apply -> epow_le.
omega.
apply -> epow_lt.
apply Zlt_succ.
apply epow_ge_0.
rewrite Rabs_pos_eq.
apply Rle_lt_trans with x.
apply Hxd.
......@@ -611,6 +624,7 @@ apply Hxu.
rewrite Rabs_pos_eq.
apply Rle_lt_trans with (bpow (emin + prec - 1)).
apply Hxu.
exists (Float beta (Zpower (radix_val beta) (prec - 1)) emin).
admit.
exact Hx.
apply -> epow_lt.
......@@ -624,14 +638,11 @@ Qed.
Theorem Rnd_NE_pt_FLT :
forall x f,
FLT_format beta emin prec f ->
( Rnd_gNE_pt FLTf x f <-> Rnd_NE_pt FLTf x f ).
Proof.
intros x f Hf.
apply Rnd_NE_pt_aux.
apply DN_UP_parity_aux.
exact DN_UP_parity_FLT_pos.
now apply -> FLT_format_generic.
Qed.
End Flocq_rnd_NE_FLT.
......
......@@ -532,42 +532,17 @@ now rewrite <- Hx.
exact HF.
Qed.
Theorem Rnd_N1_N2_pt :
forall F : R -> Prop,
forall (P1 : R -> Prop) (P2 : R -> R -> Prop),
( forall h, F h -> P1 h \/ ~P1 h ) ->
( forall f g, F f -> F g -> (P1 f \/ g = f <-> P2 f g) ) ->
forall x f,
Rnd_N1_pt F P1 x f <-> Rnd_N2_pt F P2 x f.
Proof.
intros F P1 P2 HP1 HP12 x f.
split ; intros (H, Hf) ; ( split ; [ exact H | .. ] ).
(* . *)
intros g Hg.
apply (proj1 (HP12 _ _ (proj1 H) (proj1 Hg))).
destruct Hf as [Hf|Hf].
now left.
right.
now apply Hf.
(* . *)
destruct (HP1 _ (proj1 H)) as [H1|H1].
now left.
right.
intros f2 H2.
destruct (proj2 (HP12 _ _ (proj1 H) (proj1 H2))) as [H3|H3].
now apply Hf.
now elim H1.
exact H3.
Qed.
Definition Rnd_NG_pt_unicity_prop F P :=
forall x d u,
Rnd_DN_pt F x d -> Rnd_N_pt F x d ->
Rnd_UP_pt F x u -> Rnd_N_pt F x u ->
P x d -> P x u -> d = u.
Definition Rnd_N1_pt_unicity_prop F P :=
forall x d u, Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> P d -> P u -> d = u.
Theorem Rnd_N1_pt_unicity :
forall (F : R -> Prop) (P : R -> Prop),
Rnd_N1_pt_unicity_prop F P ->
Theorem Rnd_NG_pt_unicity :
forall (F : R -> Prop) (P : R -> R -> Prop),
Rnd_NG_pt_unicity_prop F P ->
forall x f1 f2 : R,
Rnd_N1_pt F P x f1 -> Rnd_N1_pt F P x f2 ->
Rnd_NG_pt F P x f1 -> Rnd_NG_pt F P x f2 ->
f1 = f2.
Proof.
intros F P HP x f1 f2 (H1a,H1b) (H2a,H2b).
......@@ -578,63 +553,213 @@ destruct (Rnd_N_pt_DN_or_UP _ _ _ H1a) as [H1c|H1c] ;
eapply Rnd_DN_pt_unicity ; eassumption.
now apply (HP x f1 f2).
apply sym_eq.
now apply (HP x f2 f1 H2c H1c).
now apply (HP x f2 f1 H2c H2a H1c H1a).
eapply Rnd_UP_pt_unicity ; eassumption.
now apply H2b.
apply sym_eq.
now apply H1b.
Qed.
Theorem Rnd_N1_pt_monotone :
forall (F : R -> Prop) (P : R -> Prop),
Rnd_N1_pt_unicity_prop F P ->
Theorem Rnd_NG_pt_monotone :
forall (F : R -> Prop) (P : R -> R -> Prop),
Rnd_NG_pt_unicity_prop F P ->
forall x y f g : R,
Rnd_N1_pt F P x f -> Rnd_N1_pt F P y g ->
Rnd_NG_pt F P x f -> Rnd_NG_pt F P y g ->
x <= y -> f <= g.
Proof.
intros F P HP x y f g (Hf,Hx) (Hg,Hy) [Hxy|Hxy].
now apply Rnd_N_pt_monotone with F x y.
apply Req_le.
rewrite <- Hxy in Hg, Hy.
eapply Rnd_N1_pt_unicity ; try split ; eassumption.
eapply Rnd_NG_pt_unicity ; try split ; eassumption.
Qed.
Definition Rnd_N2_pt_unicity_prop F P :=
forall x d u, Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> P d u -> P u d -> d = u.
Theorem Rnd_NG_pt_sym :
forall (F : R -> Prop) (P : R -> R -> Prop),
( forall x, F x -> F (-x) ) ->
( forall x f, P x f -> P (-x) (-f) ) ->
forall x f : R,
Rnd_NG_pt F P (-x) (-f) -> Rnd_NG_pt F P x f.
Proof.
intros F P HF HP x f (H1,H2).
split.
now apply Rnd_N_pt_sym.
destruct H2 as [H2|H2].
left.
rewrite <- (Ropp_involutive x), <- (Ropp_involutive f).
now apply HP.
right.
intros f2 Hxf2.
rewrite <- (Ropp_involutive f).
rewrite <- H2 with (-f2).
apply sym_eq.
apply Ropp_involutive.
apply Rnd_N_pt_sym.
exact HF.
now rewrite 2!Ropp_involutive.
Qed.
Theorem Rnd_N2_pt_unicity :
Theorem Rnd_NG_unicity :
forall (F : R -> Prop) (P : R -> R -> Prop),
Rnd_N2_pt_unicity_prop F P ->
forall x f1 f2 : R,
Rnd_N2_pt F P x f1 -> Rnd_N2_pt F P x f2 ->
f1 = f2.
Rnd_NG_pt_unicity_prop F P ->
forall rnd1 rnd2 : R -> R,
Rnd_NG F P rnd1 -> Rnd_NG F P rnd2 ->
forall x, rnd1 x = rnd2 x.
Proof.
intros F P HP x f1 f2 (H1a,H1b) (H2a,H2b).
destruct (Rnd_N_pt_DN_or_UP _ _ _ H1a) as [H1c|H1c] ;
destruct (Rnd_N_pt_DN_or_UP _ _ _ H2a) as [H2c|H2c].
intros F P HP rnd1 rnd2 H1 H2 x.
now apply Rnd_NG_pt_unicity with F P x.
Qed.
Theorem Rnd_NA_NG_pt :
forall F : R -> Prop,
F 0 ->
forall x f,
Rnd_NA_pt F x f <-> Rnd_NG_pt F (fun x f => Rabs x <= Rabs f) x f.
Proof.
intros F HF x f.
destruct (Rle_or_lt 0 x) as [Hx|Hx].
(* *)
split ; intros (H1, H2).
(* . *)
assert (Hf := Rnd_N_pt_pos F HF x f Hx H1).
split.
exact H1.
destruct (Rnd_N_pt_DN_or_UP _ _ _ H1) as [H3|H3].
(* . . *)
right.
intros f2 Hxf2.
specialize (H2 _ Hxf2).
destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H4|H4].
eapply Rnd_DN_pt_unicity ; eassumption.
apply (HP x f1 f2 H1c H2c).
now apply H1b.
now apply H2b.
apply sym_eq.
apply (HP x f2 f1 H2c H1c).
now apply H2b.
now apply H1b.
apply Rle_antisym.
rewrite Rabs_pos_eq with (1 := Hf) in H2.
rewrite Rabs_pos_eq in H2.
exact H2.
now apply Rnd_N_pt_pos with F x.
apply Rle_trans with x.
apply H3.
apply H4.
(* . . *)
left.
rewrite Rabs_pos_eq with (1 := Hf).
rewrite Rabs_pos_eq with (1 := Hx).
apply H3.