proposition: Theorem absurd_intersect_aa : forall z : R, forall xi yi : FF, ABS z xi -> ABS z yi -> Flt2 (upper xi) (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 _ _ _ (proj2 (proj2 Hx)) H). clear H. intro H. generalize (Rlt_le_trans _ _ _ H (proj1 (proj2 Hy))). clear H. intro H. elim (Rlt_irrefl _ H). Qed.
imports: Gappa_common Gappa_pred_nzr