proposition: Theorem neg_fix : forall x : R, forall xn zn : Z, FIX x xn -> Zle_bool zn xn = true -> FIX (-x)%R zn.
proof: Proof. intros x xn zn [fx [Hx1 Hx2]] Hb. generalize (Zle_bool_imp_le _ _ Hb). clear Hb. intro H1. exists (Fopp2 fx). split. rewrite <- Hx1. apply Fopp2_correct. now apply Z.le_trans with xn. Qed.
imports: Flocq(Core Sterbenz) Gappa_common Gappa_round_aux