proposition: Theorem fix_of_singleton_bnd : forall x : R, forall xi : FF, forall n : Z, ABS x xi -> fix_of_singleton_bnd_helper xi n = true -> FIX x n.
proof: Proof. intros x xi n (_, (Hx1, Hx2)) Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H3). generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Zeq_bool_correct_t _ _ H1). clear H1. intro H1. generalize (Zeq_bool_correct_t _ _ H2). clear H2. intro H2. generalize (Zle_bool_imp_le _ _ H3). clear H3. intro H3. assert (float2R (lower xi) = Rabs x). apply Rle_antisym. exact Hx1. replace (lower xi) with (upper xi). exact Hx2. apply sym_equal. induction (lower xi). induction (upper xi). exact (f_equal2 _ H1 H2). unfold Rabs in H. induction (Rcase_abs x). exists (Fopp2 (lower xi)). split. rewrite Fopp2_correct. rewrite <- (Ropp_involutive x). apply Ropp_eq_compat. exact H. exact H3. exists (lower xi). exact (conj H H3). Qed.
imports: Flocq(Core Sterbenz) Gappa_common Gappa_round_aux