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