proposition: Theorem absurd_intersect_rr : forall z1 z2 : R, forall xi yi : FF, REL z1 z2 xi -> REL z1 z2 yi -> NZR z2 -> Flt2 (upper xi) (lower yi) = true -> False.
proof: Proof. intros z1 z2 xi yi (xe,(Hx1,Hx2)) (ye,(Hy1,Hy2)) Hz Hb. generalize (Flt2_correct _ _ Hb). clear Hb. intro H. generalize (Rle_lt_trans _ _ _ (proj2 Hx1) H). clear H. intro H. replace xe with ye in H. generalize (Rlt_le_trans _ _ _ H (proj1 Hy1)). clear H. intro H. elim (Rlt_irrefl _ H). clear H. apply sym_eq. apply Rplus_eq_reg_l with 1%R. apply Rmult_eq_reg_l with (2 := Hz). now rewrite <- Hx2. Qed.
imports: Gappa_common Gappa_pred_bnd