在Dafny中如何证明自然数除法与实数Floor除法的等价性？

我目前卡在一个Dafny引理的证明上，想寻求大家的帮助：

lemma NatDivision(a: nat, b: nat) 
  requires b != 0 
  ensures a / b == (a as real / b as real).Floor 

我完全摸不着头绪——这看起来几乎就是公理级别的性质。要是能找到对应的相关公理，我就能以此为基础展开证明，但我翻遍Dafny源码都没找到自然数除法的公理。《This Is Boogie 2》里提到Boogie要求用户自行定义这类公理，所以我猜测这些公理可能藏在某个C#代码实现里？

（补充下背景：我本来是想通过一种方法证明自然数的(a + n * b) % b == a % b这个性质，现在已经有一个近乎完成的Dafny证明了。）

内容的提问来源于stack exchange，提问作者Jason Orendorff