fraczeq12 Show Code edit
## Equivalence for </> ##
thm (fraczeq12 () () (-> (/\ (z.= A B) (z.= C D)) (= (</> A C) (</> B D)))
A B C fraczeq1
(-> (z.= A B) (= (</> A C) (</> B C)))
C D B fraczeq2
(-> (z.= C D) (= (</> B C) (</> B D)))
anim12i
(-> (/\ (z.= A B) (z.= C D)) (/\ (= (</> A C) (</> B C)) (= (</> B C) (</> B D))))
(</> A C) (</> B C) (</> B D) eqtr
(-> (/\ (= (</> A C) (</> B C)) (= (</> B C) (</> B D))) (= (</> A C) (</> B D)))
syl
(-> (/\ (z.= A B) (z.= C D)) (= (</> A C) (</> B D)))
)
edit