Proof of proveit.numbers.ordering.transitivity_less_eq_less_eq theorem

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

%proving transitivity_less_eq_less_eq

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

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

defaults.assumptions = transitivity_less_eq_less_eq.all_conditions()

defaults.assumptions:

less_eq_def

 ⊢  

x_leq_y__expanded = less_eq_def.instantiate({x:x, y:y}).derive_right_via_equality()

x_leq_y__expanded:  ⊢  

x_less_y, x_eq_y = x_leq_y__expanded.operands

x_less_y:

x_eq_y:

transitivity_less_less_eq

 ⊢  

x_less_z = transitivity_less_less_eq.instantiate({x:x, y:y, z:z}, assumptions=defaults.assumptions+(x_less_y,))

x_less_z: ,  ⊢  

x_less_z.derive_relaxed()

,  ⊢  

x_eq_y.sub_left_side_into(LessEq(y, z), assumptions=defaults.assumptions+(x_eq_y,))

,  ⊢  

x_leq_y__expanded.derive_via_dilemma(LessEq(x, z))

,  ⊢  

%qed

proveit.numbers.ordering.transitivity_less_eq_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, 15	,  ⊢
	: , :
11	instantiation	16, 23, 17	,  ⊢
	: , : , :
12	conjecture		⊢
	proveit.logic.booleans.in_bool_if_true
13	instantiation	18, 19, 20	⊢
	: , :
14	conjecture		⊢
	proveit.numbers.ordering.relax_less
15	instantiation	21, 22, 23	,  ⊢
	: , : , :
16	theorem		⊢
	proveit.logic.equality.sub_left_side_into
17	assumption		⊢
18	theorem		⊢
	proveit.logic.equality.rhs_via_equality
19	assumption		⊢
20	instantiation	24	⊢
	: , :
21	conjecture		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
22	assumption		⊢
23	assumption		⊢
24	axiom		⊢
	proveit.numbers.ordering.less_eq_def