具有此引理
Lemma my_lemma n : n %/ 4 * 4 + n %% 4 * 5 - n %% 4 * 4 = n.
Proof.
(* ? *)
(* n %/ 4 * 4 + n %% 4 = n. *)
symmetry. apply: divn_eq n 4.
Qed.
如何将n %% 4 * 5 - n %% 4 * 4转换为n %% 4？然后将是小菜一碟。
为了解决这个问题，ssreflect中的惯用方法是使用所有关于手头算术的定理进行重写。这需要一些搜索。我建议您广泛使用Search命令。
第一个障碍是您的公式包含(A + B - C)，与(A + (B - C))不同，这是由于截断减法的特殊行为。要在两者之间转换，您可以寻找一个定理。我键入了以下Search命令。
Search (_ + _ - _).
在列出的定理中，我对addnBA（加法和减法之间的联系）感到满意，但是这个引理有一个附带条件，我想首先证明一下。因此，我使用以下重写命令。
rewrite -addnBA; last first.
这里，我想在比较中排除乘法。我使用下面的Search命令寻找一个包含该模式的定理。
搜索_（_ * _ <= _ * _）。
请注意此_命令中的第一个Search模式，这一点很重要，如果不包括它，则仅列出一些有趣的定理，而我们想要的定理将不会出现。我要的是leq_mul2l
我以以下方式执行此证明：
by rewrite -leq_mul2l orbC.
在rewrite -leq_mul2l之后，该语句是_ || _语句（布尔析取），并且右侧显然是真正的模运算（在ssreflect中），通过换相该布尔析取，我使目标可以是直接解决，无需费力。
现在，我们得出乘法与减法的分布性。搜索命令在这里使用起来比较棘手，因为分配律用关键字来处理。
Search (_ * (_ - _)).
没有给出任何有用的结果，但是ssrnat中提供了有关命名模式的有用文档。它告诉我们，当减法是次要运算时，B很可能会出现在定理名称中。在这里，我们想要一个关于自然数的定理，所以它应该在ssrnat中，所以我尝试以下方法。
Search "B" in ssrnat.
这告诉我，有些定理的陈述依赖于left_distributive和right_distributive之类的概念。您可以通过打印这些概念来理解它们。
Print right_distributive.
从长远来看，您倾向于记住经常使用的定理的名称，所以在我的情况下，我知道我将要使用mulnBr，因为减法是在乘法的右边，我们正在努力与自然数。 math-comp库在设计时特别注意命名的规律性。
因此，我们现在可以按以下方式完成修改：
rewrite -mulnBr muln1.
您最终可以应用想要应用的引理。
完整脚本如下：
Lemma my_lemma n : n %/ 4 * 4 + n %% 4 * 5 - n %% 4 * 4 = n.
Proof.
symmetry.
rewrite -addnBA; last first.
by rewrite leq_mul2l orbC.
rewrite -mulnBr muln1.
apply: divn_eq n 4.
Qed.