proposition: Lemma flt_abs_aux : forall x : R, forall xn : positive, FLT (Rabs x) xn <-> FLT x xn.
proof: Proof. intros x xn. unfold Rabs. case Rcase_abs ; intros Hx. 2: easy. split ; intros [[mx ex] [Hx1 Hx2]] ; exists (Float2 (Z.opp mx) ex) ; split ; simpl. rewrite <- (Ropp_involutive x), <- Hx1. apply F2R_Zopp. now rewrite Zabs_Zopp. rewrite <- Hx1. apply F2R_Zopp. now rewrite Zabs_Zopp. Qed.
imports: Flocq(Core Sterbenz) Gappa_common Gappa_round_aux