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_eq_less
defaults.assumptions = transitivity_less_eq_less.all_conditions()
less_eq_def
spec_l_e_d = less_eq_def.instantiate({x:x, y:y})
spec_l_e_d.derive_right_via_equality()
xeq_y = Less(x,z).prove(assumptions = (Equals(x,y), Less(y,z)))
xless_y = Less(x,z).prove(assumptions = (Less(x,y), Less(y,z)))
spec_l_e_d.rhs.derive_via_dilemma(Less(x,z))
%qed