Séance de cours
Cette séance de cours introduit Coq, un assistant de preuve, se concentrant sur le théorème et le_comm, qui indique que pour toutes les propositions P et Q, si P et Q sont vraies, alors Q et P sont également vraies. La séance de cours couvre le processus de prouver ce théorème étape par étape à l'aide de l'assistant de preuve de Coq.