Proof of proveit.numbers.ordering.symmetric_less_eq theorem

import proveit
from proveit import defaults
from proveit.logic.equality  import equals_symmetry
from proveit import x, y, z
from proveit.logic import Equals, Or, InSet, Boolean, And, Not
from proveit.numbers import LessEq, Less, Real
from proveit.numbers.ordering  import less_eq_def, transitivity_less_less
theory = proveit.Theory() # the theorem's theory

%proving symmetric_less_eq

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

defaults.assumptions = symmetric_less_eq.all_conditions()

defaults.assumptions:

less_eq_def

 ⊢  

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

spec_l_e_dxy:  ⊢  

spec_l_e_dxy.lhs.evaluation()

 ⊢  

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

spec_l_e_dyx:  ⊢  

spec_l_e_dyx.derive_right_via_equality()

 ⊢  

xlylx = And(Less(x,y),Less(y,x)).evaluation(assumptions = [Less(x,y), Not(Less(y,x))])

xlylx: ,  ⊢  

ylxly = And(Less(y,x), Less(x,y)).evaluation(assumptions = [Less(y,x), Not(Less(x,y))])

ylxly: ,  ⊢  

xlyeqx = And(Less(x,y), Equals(y,x)).evaluation(assumptions = [Less(x,y), Not(Equals(y,x))])

xlyeqx: ,  ⊢  

xeqylx = And(Equals(x,y), Less(y,x)).evaluation(assumptions = [Equals(x,y), Not(Less(y,x))])

xeqylx: ,  ⊢  

equals_symmetry

 ⊢  

spec_e_s = equals_symmetry.instantiate({x:x, y:y})

spec_e_s:  ⊢  

spec_l_e_dxy.rhs.derive_via_dilemma(Equals(x,y), assumptions = [Equals(y,x), InSet(x, Real), InSet(y, Real)])

, ,  ⊢  

spec_l_e_dyx.rhs.derive_via_dilemma(Equals(y,x), assumptions = [Equals(x,y), InSet(x, Real), InSet(y, Real)])

, ,  ⊢