verification - Dafny カウント < サイズを証明する方法

Question

私は現在ダフニーを学んでいます。私はレンマに完全に混乱しており、その使い方がわかりません。チュートリアルはそれほど役に立ちません。どのように証明すればよいかを証明したい場合はどうすればよいです count(a) <= |a| か。助けてくれてありがとう。

function count(a: seq<bool>): nat
ensures count(a) <= |a|;
{
   if |a| == 0 then 0 else
   (if a[0] then 1 else 0) + count(a[1..])
}