proposition: Lemma is_empty_correct : forall xi x, contains (convert xi) x -> is_empty xi = true -> False.
proof: Proof. intros [|xl xu]. easy. intros x. simpl. rewrite F.cmp_correct. rewrite F.valid_lb_correct, F.valid_ub_correct. destruct x as [|x]. { now destruct F.classify ; destruct F.classify. } assert (H: (1 <= x <= 0)%R -> true = true -> False). { intros H _. apply (Rlt_not_le 1 0 Rlt_0_1). now apply Rle_trans with x. } destruct F.classify ; destruct F.classify ; try easy. destruct F.toX as [|xlr]. easy. destruct F.toX as [|xur]. easy. simpl. intros H'. case Rcompare_spec ; try easy. intros K _. apply Rlt_not_le with (1 := K). now apply Rle_trans with x. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval