<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 13 January 2015 at 12:47, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></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<n→n∸m>0 {0} {suc n} _ = suc>0<br>
m<n→n∸m>0 {0} {0} ()<br>
m<n→n∸m>0 {suc m} {suc n} (s≤s suc-m≤n) = m<n→n∸m>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<n→n∸m>0 : ∀ {m n} → m < n → n ∸ m > 0<br>m<n→n∸m>0 (s≤s z≤n) = s≤s z≤n<br>m<n→n∸m>0 (s≤s (s≤s h)) = m<n→n∸m>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>