Proofgold Proposition

wceq catan (cmpt (λ x0 . cdif cc (cpr (cneg ci) ci)) (λ x0 . co (co ci c2 cdiv) (co (cfv (co c1 (co ci (cv x0) cmul) cmin) clog) (cfv (co c1 (co ci (cv x0) cmul) caddc) clog) cmin) cmul))

type
prop

theory
SetMM

name
df_atan

proof
PUMn8..

Megalodon
-

proofgold address
TMGgL..

creator
36377 PrCmT../383df..

owner
36377 PrCmT../383df..

term root
aa0fa..