proposition: Theorem intersect_hb : forall z : R, forall xf : float2, forall yi zi : FF, (z <= xf)%R -> BND z yi -> intersect_helper xf (lower yi) zi = true -> BND z zi.
proof: Proof. intros z xf yi zi Hx Hy Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fle2_correct _ _ H1). clear H1. intro H1. generalize (Fle2_correct _ _ H2). clear H2. intro H2. split. apply Rle_trans with (1 := H1) (2 := (proj1 Hy)). apply Rle_trans with (1 := Hx) (2 := H2). Qed.
imports: Gappa_common Gappa_decimal