Proof of proveit.numbers.number_sets.real_numbers.positive_if_in_real_pos theorem

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import x, defaults
from proveit.numbers import zero, greater
from proveit.numbers.number_sets.real_numbers import real_pos_def

%proving positive_if_in_real_pos

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
positive_if_in_real_pos:
(see dependencies)

positive_if_in_real_pos may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

$\mathbb{R}^{+} = \{r | r > 0\}_{\mathbb{R}}$

defaults.assumptions = positive_if_in_real_pos.conditions

defaults.assumptions:

from proveit.numbers.number_sets.real_numbers import real_pos_def
real_pos_def

 ⊢  

x_in_real_pos = defaults.assumptions[0]

x_in_real_pos:

x_in_real_pos_assumption = x_in_real_pos.prove()

x_in_real_pos_assumption:  ⊢  

x_in_real_pos_assumption.inner_expr().domain.substitute(real_pos_def)

 ⊢  

# %qed