dafny - いくつかの公理とプロパティが与えられた場合、プロパティの証明をどのように構築すればよいでしょうか?

Question

次の公理が与えられます。

A>=0
forall n :: n>=0 && n<N1 ==> n < A
N1 >= A

N1==ADafnyを使用してそれを証明したいと思います。

次の Dafny プログラムを試しました。

function N1(n: int,A: int):bool
  requires A>=0 && n>=0 
{
  if n==0 && A<=n
  then true else
  if n>0 
    && A<=n  
    && forall k::
       (if 0<=k && k<n 
        then A>k else true) 
  then true
  else false
}

lemma Theorem(n: int,A: int)
requires A>=0 && n>=0 && N1(n,A)
ensures n==A;
{ }

しかし、ダフニーはそれを証明できません。N1==A与えられた公理から抜け出す方法はありますか?