proposition: Theorem output_correct : forall fmt xi x, contains (convert xi) (Xreal x) -> contains_output (output fmt xi) x.
proof: Proof. intros fmt xi x. unfold output, convert. destruct xi as [|xl xu] ; try easy. assert (H: forall P : Prop, (1 <= x <= 0)%R -> P). { intros P [H1 H2]. elim (Rlt_irrefl 0). apply Rlt_le_trans with (1 := Rlt_0_1). apply Rle_trans with (1 := H1) (2 := H2). } destruct (F.valid_lb xl). 2: apply H. destruct (F.valid_ub xu). 2: apply H. clear H. simpl. unfold F.toX. intros [H1 H2]. destruct (F.toF xl) as [| |sl ml el] ; destruct (F.toF xu) as [| |su mu eu] ; try split ; first [ easy | apply Rle_trans with (1 := proj1 (output_bnd_correct fmt F.radix sl ml el)) | apply Rle_trans with (2 := proj2 (output_bnd_correct fmt F.radix su mu eu)) ]; easy. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval