rnlem Show Code edit
# Lemma used in construction of real numbers.
thm (rnlem () () (<-> (/\ (/\ ph ps) (/\ ch th)) (/\ (/\ (/\ ph ch) (/\ ps th)) (/\ (/\ ph th) (/\ ps ch)))) ph ps (/\ ch th) anandir ph ch th anandi ps ch th anandi anbi12i (/\ ps ch) (/\ ps th) ancom (/\ (/\ ph ch) (/\ ph th)) anbi2i (/\ ph ch) (/\ ph th) (/\ ps th) (/\ ps ch) an4 bitri 3bitri)
(<-> (/\ (/\ ph ps) (/\ ch th)) (/\ (/\ (/\ ph ch) (/\ ps th)) (/\ (/\ ph th) (/\ ps ch))))
edit