[Agda] Noetherian vs WellFounded

[mechvel at scico.botik.ru]

Can people, please, explain:

how can Agda treat the relation between the Noetherian property of an 
ordering _<_
and its property of WellFounded
(of Induction.WellFounded of Standard library) ?

A relation _<_ is called Noetherian iff there does not exist any 
infinite sequence descending by _<_.

The matter is that many proofs in mathematics look like this:
"This process terminates because it includes forming a descending 
sequence  a₁ > a₂ > ...,
while the relation _>_ is Noetherian
".

For example, I have to prove a certain termination, while having
* a proof for Noetherian _<_,
* a proof for DecTotalOrder for _<_,
* a certain proved bijection algorithm Carrier <--> ℕ
   (whithout preserving the ordering).

And I wonder of how to prove this termination in Agda.


* Is it possible to prove in Agda  (Noetherian ==> Wellfounded)
   for any partial ordering _<_ ?

* What additional condition (the more generic the better) can be 
sufficient for this proof?
   For example:
   a) a bijection algorithm Carrier <--> ℕ
      (whithout a given proof for preserving the ordering),
   or/and
   b) DecTotalOrder for _<_.

* Is there a counter-example for (Noetherian ==> Wellfounded) ?

* What can be the consequences of using, say,
   postulate
     Noetherian⇒WellFounded :
       ∀ (_<_ : of DecTotalOrder) → Noetherian _<_ → WellFounded _<_

   all through an applied library?


Thank you for possible explanation.

Regards,