Formalizing the trading theorem in Coq
scientific article; zbMATH DE number 2105263