We propose our work to introduce Coq into discrete mathematics teaching, allowing students to prove ZFC theorems formally. The purpose of employing Coq is to help students deepen their understanding of logical concepts rather than teaching them Coq, so we formalize the deduction system and ZFC set theory strictly following the textbook and develop several automated tactics. Students can build proofs in a textbook-style proving environment, requiring hardly any knowledge about Coq. Teaching experience shows that undergraduate students can quickly construct formal proofs of mathematical induction and Peano arithmetic using our mini ZFC theorem prover developed in Coq.