proposition: Theorem intersect_aa : forall z : R, forall xi yi zi : FF, ABS z xi -> ABS z yi -> intersect_aa_helper (upper xi) (lower yi) zi = true -> ABS z zi.
proof: Proof. intros z xi yi zi Hx Hy Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H3). generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fpos0_correct _ H1). clear H1. intro H1. generalize (Fle2_correct _ _ H2). clear H2. intro H2. generalize (Fle2_correct _ _ H3). clear H3. intro H3. split. exact H1. split. apply Rle_trans with (1 := H2) (2 := proj1 (proj2 Hy)). apply Rle_trans with (1 := proj2 (proj2 Hx)) (2 := H3). Qed.
imports: Gappa_common Gappa_pred_nzr