An exact proof term for the current goal is zero_in_unit_interval.

An exact proof term for the current goal is one_in_unit_interval.