Dafny中除法边界引理验证及除零警告问题咨询

我需要在Dafny中证明以下性质：若除法表达式(a+k)/(b+k)小于等于1，那么当a < -k时，该除法结果大于等于-1。

举个例子：

• 当a=2、b=3、k=0.1时，(2+0.1)/(3+0.1) ≤ 1成立；
• 当a=-2（满足a < -k=-0.1）时，-1 ≤ (-2+0.1)/(3+0.1)也成立。

我编写了如下引理，但遇到了问题：

lemma boundDivision (a:real, b:real, k:real)
  requires k>=0.0 && b>=0.0
  requires a <= b;
  //requires b+k >=0.0
  ensures (a+k)/(b+k) <= 1.0 ==> (a<-k ==> (-1.0 <= (a+k)/(b+k)))
  {
    //assert b+k>=0.0;
  }

遇到的问题 #

1. 该引理无法自动验证；
2. 明明b和k均为非负数，Dafny却在(a+k)/(b+k)处提示“possible division by zero”（可能除零）；
3. 后续发现实际场景中k应为严格正数，更新代码后（如下）仍无法完成验证，需要协助完成该性质的证明：

lemma boundDivision (a:real, b:real, k:real)
  requires k>0.0 && b>=0.0
  requires a <= b;
  //requires b+k >=0.0
  ensures (a+k)/(b+k) <= 1.0 ==> (a<-k ==> (-1.0 <= (a+k)/(b+k)))
  {
    //assert b+k>=0.0;
  }

内容的提问来源于stack exchange，提问作者Theo Deep