Dafny常量属性确立问题：use_a函数断言无法通过验证

我是Dafny新手，原本期望以下代码中use_a函数内的断言能够通过验证：

class A {

  const a: int

  constructor(a0: int)
    requires a0 > 100
    ensures a > 100
  {
    a := a0;
  }

  function use_a(): bool
    reads this
  {
    assert a > 100;
    a > 200
  }

}

但验证器提示Error: assertion might not hold。我的实际场景是从构造函数参数创建一个复杂常量（例如基于给定列表生成具有特定属性的映射），需要在构造函数中确立该常量的相关属性，并在类的其他地方使用这些属性。我感觉自己遗漏了某些关键点……

更新： #

基于讨论，我认为以下代码符合我的需求：

type vala = a: nat | a > 100 witness 101

class A {

  const a: vala

  constructor(a0: nat)
    requires a0 > 100
  {
    a := a0;
  }

  function use_a() : bool
  {
    assert a > 100;
    this.a > 200
  }

}

内容的提问来源于stack exchange，提问作者Sam Stainsby