fraczeq1i Show Code edit
thm (fraczeq1i () (
hyp1 (z.= A B))
(= (</> A C) (</> B C))
hyp1
(z.= A B)
A B C fraczeq1
(-> (z.= A B) (= (</> A C) (</> B C)))
ax-mp
(= (</> A C) (</> B C))
)
edit