eqcom Show Code edit
## Symmetric Property
## Rational equality is symmetric.
## For more information see the construction of the rationals.
## right('Commute', '=')
thm (eqcom () () (<-> (= A B) (= B A))
A B df-eq
(<-> (= A B) (/\ (z.= (z.* (top A) (bottom B)) (z.* (top B) (bottom A))) (<-> (z.= (bottom A) (z.0)) (z.= (bottom B) (z.0)))))
## <d 'Symmetric Property '>
(z.* (top A) (bottom B)) (z.* (top B) (bottom A)) z.eqcom
(<-> (z.= (z.* (top A) (bottom B)) (z.* (top B) (bottom A))) (z.= (z.* (top B) (bottom A)) (z.* (top A) (bottom B))))
(<-> (= A B) (/\ (z.= (z.* (top B) (bottom A)) (z.* (top A) (bottom B))) (<-> (z.= (bottom A) (z.0)) (z.= (bottom B) (z.0)))))
## </d 'Symmetric Property '>
## <d 'Commutative Biconditional '>
(z.= (bottom A) (z.0)) (z.= (bottom B) (z.0)) bicom
(<-> (<-> (z.= (bottom A) (z.0)) (z.= (bottom B) (z.0))) (<-> (z.= (bottom B) (z.0)) (z.= (bottom A) (z.0))))
(<-> (= A B) (/\ (z.= (z.* (top B) (bottom A)) (z.* (top A) (bottom B))) (<-> (z.= (bottom B) (z.0)) (z.= (bottom A) (z.0)))))
## </d 'Commutative Biconditional '>
B A df-eq bicomi
(<-> (/\ (z.= (z.* (top B) (bottom A)) (z.* (top A) (bottom B))) (<-> (z.= (bottom B) (z.0)) (z.= (bottom A) (z.0)))) (= B A))
(<-> (= A B) (= B A))