proposition: Lemma Bolzano_hyp_simp f x y: x <=r y -> (forall z, x <=r z -> z <=r y -> continuous_at f z) -> Bolzano_hyp f x y.
proof: Proof. move => xy h; move:(xy) => [rx ry _];split. + move => e ep; move: (h _ (rleR rx) xy) => cf; move: (cf e ep). move => [d da db]; ex_tac. + move => e ep; move: (h _ xy (rleR ry)) => cf; move: (cf e ep). move => [d da db]; ex_tac. + by move => z [za _] [zb _]; apply: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)