proposition: Lemma floatx_absolute_ne_sym : forall p x, (Rabs (rounding_floatx rndNE p x - x) = Rabs (rounding_floatx rndNE p (Rabs x) - Rabs x))%R.
proof: Proof. intros p x. destruct (Rle_or_lt 0 x) as [H|H]. rewrite (Rabs_right _ (Rle_ge _ _ H)). exact (refl_equal _). rewrite (Rabs_left _ H). rewrite round_NE_opp. unfold Rminus. rewrite <- Ropp_plus_distr. now rewrite Rabs_Ropp. 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