Неожиданное «возможное деление на ноль», когда известно, что значения положительные

Я хочу доказать в Дафни следующее свойство: если деление (a+k)/(b+k) меньше или равно 1; тогда, если a меньше -k, деление (a+k)/(b+k) теперь больше или равно -1.

Например, учитывая a=2, b=3 и k=0.1, мы имеем 2+0.1/3+0.1 <= 1. Но если a=-2, что меньше -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;
  }

Это не проверяется автоматически, но меня смущает тот факт, что Дафни предупреждает possible division by zero в (a+k)/(b+k). Я имею в виду, что и b, и k неотрицательны...

Что мне не хватает? Как я могу это проверить?

РЕДАКТИРОВАТЬ

Оказывается, я сохранял 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;
  }