[Agda] Total: x !<= y ==> y <= x

[Serge D. Mechveliani]

On Thu, Oct 11, 2012 at 07:18:49PM +0400, Serge D. Mechveliani wrote:
> On Wed, Oct 10, 2012 at 10:20:08AM -0700, wren ng thornton wrote:
> > On 10/10/12 11:59 AM, Serge D. Mechveliani wrote:> People,
[..]
> > > I have  ord : DecTotalOrder,
> > >          _<=_  extracted from this  ord,
> > >          ``with  x <=? y''   produced    no x-!<=-y
> > >          (I think,   x-!<=-y :  \neg x <= y )
> > >
> > > (here I replace \<= with <= ).
> > >
> > > And from this   x-!<=-y,  I need to construct  y<=x : y <= x.
>
> [..]
> The corresponding lemma coded in Agda is 
> 
>   !<=thenFlip : {c l1 l2 : Level} -> (ord : DecTotalOrder c l1 l2) ->
>                 let leq = _<=_ ord
>                 in  (x y : Carrier ord) -> \neg (leq x y) -> leq y x
> 
>   !<=thenFlip ord x y neg =   ??
> 
> (I replace the math symbols in an evident way).
> 
> Please,  what is the simplest code for it?


I am sorry for disturbance!
 
I have fixed the pattern syntax usage, and now find quite a simple
expression: 
             with  total ord x y
    ...    | inj_2 y<=x  = y<=x 
    ...    | inj_1 x<=y  with  neg x<=y 
    ...                | ()

I do not know, may be it worths adding this  !<=thenFlip  to 
Relation.Binary  of Standard library.

Regards,
Sergei