HomeIsabelle/Phabricator

cleaning proofs, use more real_asymp