<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 12 January 2015 at 13:28, 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:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div>Having the goal of  m &lt; n → n ∸ m &gt; 0   (for ℕ), <br>
<br>
and using  Standard library 0.9,  I program<br>
<br>
  lemma : ∀ n → (suc n) ∸ n ≡ 1<br>
  lemma 0       = PE.refl <br>
  lemma (suc n) = lemma n<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 {m} {n} m&lt;n = <br>
                    ≤begin  <br>
                      suc 0       ≡≤[ PE.sym $ lemma m ]<br>
                      suc m ∸ m    ≤[ ∸-mono m&lt;n (≤refl {m} PE.refl) ]  <br>
                      n ∸ m<br>
                    ≤end<br>
<br>
Here lemma looks like a complication that needs to be avoided.<br>
Is there possible a shorter implementation for the goal?</div></blockquote></div><br><div class="gmail_default" style="font-size:small">​Yes. You can pattern-match on m&lt;n.​</div><br><br clear="all"><br>-- <br><div class="gmail_signature"><div dir="ltr">Andrés<br></div></div>
</div></div>