proposition: Theorem absurd_intersect_bh : forall z : R, forall xi : FF, forall yf : float2, BND z xi -> (yf <= z)%R -> Flt2 (upper xi) yf = true -> False.
proof: Proof. intros z xi yi Hx Hy Hb. generalize (Flt2_correct _ _ Hb). clear Hb. intro H. generalize (Rle_lt_trans _ _ _ (proj2 Hx) H). clear H. intro H. generalize (Rlt_le_trans _ _ _ H Hy). clear H. intro H. elim (Rlt_irrefl _ H). Qed.
imports: Gappa_common Gappa_decimal