title: How to prove Dafny count < size
body: <p>I'm currently learning Dafny. I'm totally comfused by lemma and I dont know how to use it. The tutorial is not that helpful. What if I want to prove
  <code>count(a) &lt;= |a|</code>
  how should I do it. Thanks for helping.</p>
  
  <pre><code>function count(a: seq&lt;bool&gt;): nat
  ensures count(a) &lt;= |a|;
  {
     if |a| == 0 then 0 else
     (if a[0] then 1 else 0) + count(a[1..])
  }
  </code></pre>