proposition: Lemma round_fix_correct' : forall mode prec emin, I.extension (Xround_fix mode emin) (round_fix prec mode emin).
proof: Proof. unfold round_fix. intros mode prec emin xi [ |x] Hx ; simpl. - now apply contains_Xnan, I.add_propagate_l, contains_Xnan. - replace (Basic.round_fix mode emin x) with (x + (Basic.round_fix mode emin x - x)) by ring. apply add_correct; [easy| ]. now apply I.error_fix_correct with (x := Xreal x). Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic