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

[Serge D. Mechveliani]

People,
I have a beginner question on usage of DecTotalOrder of Standard 
library.

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.
Because I think that this a constructive reifation for a classical 
lemma for  (Total <=)  of that   not (x <= y)  ==>  y <= x.
I see in  Relation.Binary, Core:

  record IsTotalOrder ...  
         isPartialOrder : IsPartialOrder _~~_ _<=_  
         total          : Total _<=_

(here I replace some math symbols) 
                                            
  Total : forall {a l} {A : Set a} -> Rel A l -> Set _              
  Total _~_ = forall x y -> (x ~ y) \u+ (y ~ x)

, where  \u+  denotes, I think, something close to union of types. 
How to operate with a data from  (P \u+ Q) ?
what are the constructors?
Probably, one needs to apply   total <= x y :  (x <= y) \u+ (y <= x)
and then to use                x-!<=-y :  \neg x <= y 

Where  \u+  is defined in the Standard library?
It is visible a certain `combinator'  <\u+>,  with the denotation  
[ P , Q ].  I do not know of what does all this mean.

If it was not a math symbol, I could apply  grep foo *.agda.

May be, Standard Library provides somewhere a lemma, like  

 (\neg x <= y) includedInto (y <= x)   for  _<=_  from  TotalOrder ?

Thank you in advance for explanation,

------
Sergei