如何手动使用calc证明含存在变量的Dafny引理？

问题说明 #

我需要证明以下Dafny引理，但自动验证无法通过。我尝试用Dafny的calc特性做引导式证明，但不清楚如何在包含存在变量的引理中应用该特性。

Dafny引理代码 #

lemma foo(s: nat, e: nat)
  requires s < e
  ensures exists c : nat  :: s + c == e

触发的警告信息 #

无法找到该量词的触发器。没有触发器，量词可能导致验证不稳定。要消除此警告，请使用{:trigger}属性添加显式触发器。更多信息，请参考参考手册中的量词实例化规则部分。

已完成的Coq证明 #

我已经在Coq中完成了该引理的证明，但无法将其导出到Dafny环境中：

From Stdlib Require Import PeanoNat.
From Stdlib Require Import Lia.

Lemma LtIsEqPlusC : forall (b a: nat), a < b -> (exists c, a + c = b).
Proof.
  induction b; try lia.
  induction a.
  - intro G.
    assert (C: b = 0 \/ 0 < b) by lia.
    destruct C ; [ subst; exists 1 | exists (S b) ]; reflexivity.
  - intro G.
    apply Nat.succ_lt_mono in G.
    apply IHb in G.
    destruct G.
    exists x.
    lia.
Qed.

内容的提问来源于stack exchange，提问作者Daniil Iaitskov