We will prove completely_regular_space R R_standard_topology.

rewrite the current goal using metric_topology_R_bounded_metric_eq_R_standard_topology (from right to left).

An exact proof term for the current goal is (metric_spaces_completely_regular R R_bounded_metric R_bounded_metric_is_metric_on).

∎