
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 TRANSITIONAL//EN">

<HTML>

<HEAD>

  <META HTTP-EQUIV="Content-Type" CONTENT="text/html; CHARSET=UTF-8">

  <META NAME="GENERATOR" CONTENT="GtkHTML/3.30.3">

</HEAD>

<BODY>

People,<BR>

<BR>

Having the goal of&nbsp; m &lt; n &#8594; n &#8760; m &gt; 0&nbsp;&nbsp; (for &#8469;), <BR>

<BR>

and using&nbsp; Standard library 0.9,&nbsp; I program<BR>

<BR>

&nbsp; lemma : &#8704; n &#8594; (suc n) &#8760; n &#8801; 1<BR>

&nbsp; lemma 0&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; = PE.refl <BR>

&nbsp; lemma (suc n) = lemma n<BR>

<BR>

&nbsp; m&lt;n&#8594;n&#8760;m&gt;0 : &#8704; {m n} &#8594; m &lt; n &#8594; n &#8760; m &gt; 0<BR>

&nbsp; m&lt;n&#8594;n&#8760;m&gt;0 {m} {n} m&lt;n = <BR>

&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; &#8804;begin&nbsp; <BR>

&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; suc 0&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; &#8801;&#8804;[ PE.sym $ lemma m ]<BR>

&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; suc m &#8760; m&nbsp;&nbsp;&nbsp; &#8804;[ &#8760;-mono m&lt;n (&#8804;refl {m} PE.refl) ]&nbsp; <BR>

&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; n &#8760; m<BR>

&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; &#8804;end<BR>

<BR>

Here lemma looks like a complication that needs to be avoided.<BR>

Is there possible a shorter implementation for the goal?<BR>

<BR>

Thanks,<BR>

<BR>

------<BR>

Sergei

</BODY>

</HTML>