In this paper we reason about knowledge in multi-agent systems composed of intelligent agents by using Coq - a formal proof management system. We use the dynamic logic of common knowledge which is an extension of common knowledge logic with a dynamic operator that enables us to express the epistemic consequences of epistemic actions. The epistemic actions of agents are actions that change agents’ knowledge about the state of the system, knowledge about other agents’ knowledges, higher-order agents’ knowledge and so on, up to common knowledge. In existing papers about dynamic epistemic logic using Coq, the notion of epistemic actions is not sufficiently elaborated and it is simply assumed that it is quite clear how these events actually produce new knowledge for agents. Our paper is a first attempt to use Coq to “explain” how internal structures of epistemic actions produce changes in the epistemic properties of a considered system. For this purpose and in order to define epistemic actions as a special type in Coq, we use the well known action model introduced in dynamic epistemic logic. It allows us to add a general form of interchange principle which connects knowledge and time in systems with perfect recall. As an example we consider knowledge games defined by van Ditmarsch, which are card games where players have limited information about other players' cards, and gradually gain information about the states by observing the epistemic actions. To the best of our knowledge, there are no papers in which such games are considered using a Coq proof assistant. We use an axiomatization of the card games as given by van Ditmarsch but in an extended form since some axioms are required in our approach. Due to a deficit in practical implementations grounded in theory which would enable players to compute their knowledge in any state of the game, we provide such implementation at the end of paper.