fracExpandEq Show Code edit
thm (fracExpandEq () () (z.= A (</> (top A) (bottom A)))
A z.opexpand
(z.= A (z.<,> (z.head A) (z.tail A)))
A df-bottom z.eqcomi
(z.= (z.tail A) (bottom A))
(z.head A) z.opeq2i
(z.= (z.<,> (z.head A) (z.tail A)) (z.<,> (z.head A) (bottom A)))
z.EqReplaceEq1
(z.= A (z.<,> (z.head A) (bottom A)))
A df-top z.eqcomi
(z.= (z.head A) (top A))
ZeqReplaceEq1Op0
(z.= A (z.<,> (top A) (bottom A)))
(top A) (bottom A) df-fraction z.eqcomi
(z.= (z.<,> (top A) (bottom A)) (</> (top A) (bottom A)))
z.EqReplaceEq1
(z.= A (</> (top A) (bottom A)))
)
edit