Proof of proveit.numbers.ordering.transitivity_less_less_eq theorem

import proveit
from proveit import defaults
from proveit import x, y, z
from proveit.logic import Equals
from proveit.numbers import Less
from proveit.numbers.ordering  import less_eq_def
theory = proveit.Theory() # the theorem's theory

%proving transitivity_less_less_eq

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

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

defaults.assumptions = transitivity_less_less_eq.all_conditions()

defaults.assumptions:

spec_l_e_d = less_eq_def.instantiate({x:y, y:z})

spec_l_e_d:  ⊢  

spec_l_e_d.derive_right_via_equality()

 ⊢  

yeq_z = Less(x,z).prove(assumptions = (Equals(y,z), Less(x,y)))

yeq_z: ,  ⊢  

yless_z = Less(x,z).prove(assumptions = (Less(y,z), Less(x,y)))

yless_z: ,  ⊢  

spec_l_e_d.rhs.derive_via_dilemma(Less(x,z))

,  ⊢  

%qed

proveit.numbers.ordering.transitivity_less_less_eq has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3, 4, 13, 5, 6	,  ⊢
	: , : , :
2	theorem		⊢
	proveit.logic.booleans.disjunction.singular_constructive_dilemma
3	instantiation	7, 9	⊢
	: , :
4	instantiation	8, 9	⊢
	: , :
5	deduction	10	⊢
6	deduction	11	⊢
7	axiom		⊢
	proveit.logic.booleans.disjunction.left_in_bool
8	axiom		⊢
	proveit.logic.booleans.disjunction.right_in_bool
9	instantiation	12, 13	⊢
	:
10	instantiation	14, 17, 15	,  ⊢
	: , : , :
11	instantiation	16, 17, 18	,  ⊢
	: , : , :
12	conjecture		⊢
	proveit.logic.booleans.in_bool_if_true
13	instantiation	19, 20, 21	⊢
	: , :
14	axiom		⊢
	proveit.numbers.ordering.transitivity_less_less
15	assumption		⊢
16	theorem		⊢
	proveit.logic.equality.sub_right_side_into
17	assumption		⊢
18	assumption		⊢
19	theorem		⊢
	proveit.logic.equality.rhs_via_equality
20	assumption		⊢
21	instantiation	22	⊢
	: , :
22	axiom		⊢
	proveit.numbers.ordering.less_eq_def