proposition: Theorem floatx_relative_n : forall c p x zi, floatx_relative_n_helper p zi = true -> REL (rounding_floatx (Znearest c) p x) x zi.
proof: Proof. intros c p x zi Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fle2_correct _ _ H1). unfold float2R. simpl. rewrite (F2R_Zopp _ 1%Z), F2R_bpow. clear H1. intro H1. generalize (Fle2_correct _ _ H2). unfold float2R. simpl. rewrite F2R_bpow. clear H2. intro H2. destruct (relative_error_N_FLX_ex radix2 (Zpos p) (refl_equal _) c x) as (eps, (Hr1, Hr2)). exists eps. refine (conj _ Hr2). rewrite <- (bpow_plus radix2 (-1)%Z) in Hr1. rewrite (Zplus_comm (- Zpos p)), Zplus_assoc in Hr1. split. apply Rle_trans with (1 := H1). apply Ropp_le_cancel. rewrite Ropp_involutive. apply Rle_trans with (2 := Hr1). rewrite <- Rabs_Ropp. apply Rabs_idem. apply Rle_trans with (2 := H2). apply Rle_trans with (2 := Hr1). apply Rabs_idem. Qed.
imports: Coq(Bool ZArith Reals Lia) Flocq(Core Digits Round Relative) Gappa_definitions Gappa_dyadic Gappa_pred_bnd Gappa_round_def Gappa_round_aux Gappa_round