The goal of this contribution is to provide worksheets in Coq for students to learn about divisibility and binomials. These basic topics are a good case study as they are widely taught in the early academic years (or before in France). We present here our technical and pedagogical choices, the numerous exercises we developed and a small experiment we conducted on two students. As expected, it required additional {\Coq} material such as other lemmas and dedicated tactics. The worksheets are freely available and flexible in several ways.

翻译：本文旨在提供一套Coq教学材料，帮助学生掌握整除性与二项式定理的相关知识。这两个基础数学主题作为典型案例，在高等教育初期（法国教育体系中甚至更早阶段）已被广泛讲授。本文详细阐述了我们在技术实现与教学设计上的考量，展示了所开发的大量配套习题，并汇报了针对两名学生开展的小规模教学实验。如预期所示，该教学方案需要补充额外的Coq相关材料，包括辅助引理与专用证明策略。本套教学材料以开源形式发布，并在多个维度上具备可扩展性。