<div dir="ltr"><div>Hi,</div><div> </div><div>This time I&#39;m writing to ask you for some help to understand what&#39;s going on with the following code. I&#39;m using a sized definition of natural numbers as part of a more general proof about logarithms. In particular, I don&#39;t understand why the last sentence is failing. I&#39;ve noticed that if I define a &quot;subtype : {i : Size} -&gt; SNat {i} -&gt; SNat {up i}&quot; function and then I replace the last sentence in function &quot;/2&quot; by &quot;(suc (suc n)) /2 = suc (subtype (n /2))&quot; then I&#39;m able to prove &quot;m/2&lt;=n/2&quot; using an auxiliary lemma &quot;subtype&lt;= : {i : Size}{m : SNat {i}}{n : SNat} -&gt; m &lt;= n -&gt; subtype m &lt;= subtype n&quot;.</div><div> </div><div><div>Thanks in advance,</div><div> </div><div>Bruno</div> </div><div> </div><div>module SNat where</div><div> </div><div>open import Size</div><div> </div><div>data SNat : {i : Size} -&gt; Set where<br>  zero : {i : Size} -&gt; SNat {up i}<br>  suc  : {i : Size} -&gt; SNat {i} -&gt; SNat {up i}</div><div> </div><div>data _&lt;=_ : {i : Size} -&gt; SNat {i} -&gt; SNat -&gt; Set where<br>  z&lt;=n : {i : Size}(n : SNat) -&gt; _&lt;=_ {up i} zero n<br>  s&lt;=s : {i : Size}{m : SNat {i}}{n : SNat} -&gt; m &lt;= n -&gt; suc m &lt;= suc n</div><div> </div><div>_/2 : {i : Size} -&gt; SNat {i} -&gt; SNat {i}<br>zero /2 = zero<br>(suc zero) /2 = zero<br>(suc (suc n)) /2 = suc (n /2)</div><div> </div><div>m/2&lt;=n/2 : {i : Size}{m : SNat {i}}{n : SNat} -&gt; m &lt;= n -&gt; (m /2) &lt;= (n /2)<br>m/2&lt;=n/2 (z&lt;=n n) = z&lt;=n (n /2)<br>m/2&lt;=n/2 (s&lt;=s (z&lt;=n n)) = z&lt;=n (suc n /2)<br>m/2&lt;=n/2 (s&lt;=s (s&lt;=s m&lt;=n)) = s&lt;=s (m/2&lt;=n/2 m&lt;=n)</div></div>