An unexpected 'possible division by zero' when values are known to be positive

Question

I want to prove the following property in Dafny: if a division (a+k)/(b+k) is smaller or equal than 1; then if a is smaller than -k, the division (a+k)/(b+k) is now greater or equal than -1.

For instance, given a=2,b=3 and k=0.1, we have 2+0.1/3+0.1 <= 1. But if a=-2, which holds to be smaller than -k=-0.1, then -1 <= -2+0.1/3+0.1.

Thus, I consider the following lemma:

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;
  }

It does not automatically verify, but what actually makes me confused is the fact that Dafny warns possible division by zero in (a+k)/(b+k). I mean, both b and k are non-negative...

What am I missing? How can I verify this?

EDIT

It turns out I was keeping k non-negative, instead of strictly positive which was, indeed, its usage. I am leaving my question in case someone can help me prove the property. Code is now as follows:

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;
  }

Answer 1

The property seems wrong. If you use VSCode, right-click and ask for counter examples. You might need to add more assertions to ensure the counter-examples are meaningful, but consider:

a = -3
b = 0
k = 1

Then your postcondition does not hold