forall abc的coq证明:nat,b> = c - > a + b - c = a +(b - c)

Question

有人知道以下定理的Coq的任何标准库中的证明吗？如果有的话,我找不到它.

forall abc:nat,b> = c - > a + b - c = a +(b - c)

提前谢谢,马库斯.

Answer 1

标准库中不太可能存在某些特定的配方.特别是,对于常规的Presburger算法,有一个完整的强大策略,即omega:

Require Import Omega.

Theorem t : forall a b c: nat, b >= c -> a + b - c = a + (b - c).
Proof.
  intros. omega.
Qed.