Proof of proveit.logic.equality.not_equals_symmetry theorem

import proveit
from proveit import defaults
from proveit import x, y
from proveit.logic.equality  import equals_symmetry
theory = proveit.Theory() # the theorem's theory

%proving not_equals_symmetry

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

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

defaults.assumptions = not_equals_symmetry.conditions

defaults.assumptions:

x_neq_y = defaults.assumptions[0]

x_neq_y:

not__x_eq_y = x_neq_y.unfold()

not__x_eq_y:  ⊢  

equals_symmetry

 ⊢  

# substitute x=y with y=x within Not(x=y)
equals_symmetry.instantiate({x:x, y:y}).sub_left_side_into(not__x_eq_y.inner_expr().operand)

 ⊢  

%qed

proveit.logic.equality.not_equals_symmetry has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3	⊢
	: , :
2	theorem		⊢
	proveit.logic.equality.fold_not_equals
3	instantiation	4, 5, 6	⊢
	: , : , :
4	theorem		⊢
	proveit.logic.equality.sub_left_side_into
5	instantiation	7, 8	⊢
	: , :
6	instantiation	9	⊢
	: , :
7	conjecture		⊢
	proveit.logic.equality.unfold_not_equals
8	assumption		⊢
9	axiom		⊢
	proveit.logic.equality.equals_symmetry