so far done up to r406 of [the Isabelle formalisation](/formare/auctions/blob/master/isabelle/Auction).