proposition: Theorem intersect_rr : forall z1 z2 : R, forall xi yi zi : FF, REL z1 z2 xi -> REL z1 z2 yi -> intersect_rr_helper (upper xi) (lower yi) zi = true -> REL z1 z2 zi.
proof: Proof. intros z1 z2 xi yi zi (xe,(Hx1,Hx2)) (ye,(Hy1,Hy2)) Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H3). generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). apply Fle2_correct in H1. apply Fle2_correct in H2. apply Fle2_correct in H3. case (Req_dec z2 0) ; intro. exists (float2R (lower zi)). split. split. apply Rle_refl. exact H1. rewrite Hx2. rewrite H. repeat rewrite Rmult_0_l. apply refl_equal. exists xe. split. split. apply Rle_trans with (1 := H2). replace xe with ye. apply Hy1. apply Rplus_eq_reg_l with 1%R. apply Rmult_eq_reg_l with (2 := H). now rewrite <- Hy2. now apply Rle_trans with (2 := H3). exact Hx2. Qed.
imports: Gappa_common Gappa_pred_bnd