<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 13 January 2015 at 12:47, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div id=":f2" class="" style="overflow:hidden">Thank you.<br>
Indeed:<br>
<br>
 m&lt;n→n∸m&gt;0 {0}     {suc n} _             =  suc&gt;0<br>
 m&lt;n→n∸m&gt;0 {0}     {0}     ()<br>
 m&lt;n→n∸m&gt;0 {suc m} {suc n} (s≤s suc-m≤n) =  m&lt;n→n∸m&gt;0 {m} {n} suc-m≤n</div></blockquote></div><br><div class="gmail_default" style="font-size:small">​A version using only two equations:<br><br>​m&lt;n→n∸m&gt;0 : ∀ {m n} → m &lt; n → n ∸ m &gt; 0<br>m&lt;n→n∸m&gt;0 (s≤s z≤n)     = s≤s z≤n<br>m&lt;n→n∸m&gt;0 (s≤s (s≤s h)) = m&lt;n→n∸m&gt;0 (s≤s h)<br><br></div><br>-- <br><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr">Andrés</div></div></div></div>
</div></div>