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