Proof of proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational theorem

import proveit
from proveit import Lambda
from proveit import k, q, x, y, A, B, P, S, Py, Qy
# SOME STUFF COMMENTED OUT TEMPORARILY TO ALLOW COMPILATION AFTER MASTER MERGED
# INTO THE CRAFT_EDITS_CONTAINMENT_DEMOS BRANCH WHICH ALSO REMOVED THE
# COMPREHENSION THEOREMS
# from proveit.logic import iter_q1k
from proveit.logic.sets.inclusion  import proper_subset_def, subset_eq_def
from proveit.numbers import one, zero, Less, greater, Rational, RationalPos
from proveit.numbers.number_sets.rational_numbers  import rationals_def, rationals_pos_def
# from proveit.logic.sets.comprehension import comprehension_is_subset
theory = proveit.Theory() # the theorem's theory

%proving rational_pos_within_rational

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

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

proper_subset_def

 ⊢  

subset_def_spec = proper_subset_def.instantiate({A:RationalPos, B:Rational})

subset_def_spec:  ⊢  

subset_eq_def

 ⊢  

subset_eq_def_spec = subset_eq_def.instantiate({A:RationalPos, B:Rational})

subset_eq_def_spec:  ⊢  

rationals_pos_def

 ⊢  

rationals_pos_def_r_h_s = rationals_pos_def.rhs

rationals_pos_def_r_h_s:

# comprehension_is_subset

# comprehension_is_subset_spec = comprehension_is_subset.instantiate(
#         {k:one, S:Rational, QQ:[Lambda(q, greater(q, zero))]}, relabel_map={y:q})

# rationals_pos_def.sub_left_side_into(comprehension_is_subset_spec)

# %qed