[Agda] `<' reasoning

[Sergei Meshveliani]

People,

I meet the following difficulty in Agda reasoning about _<_. 

For  Nat,  it is all right, because  m < n  is defined as  suc m ≤ n, 
and it works the construct 

 e[1]<e[n] =
     begin suc e[1]    ≤⟨ .. ⟩
           ...
           ...         ≡⟨ .. ⟩
           ...
           e[n]
     ∎

formed with standard functions   
                     begin_ , _∎ , _≡⟨_⟩_ , _≤⟨_⟩_ 

But there are domains without  suc  operator (agreed with _≤_, _<_).
For example, consider the proof

----------------------------------------------
postulate  bs1<bs'1 :  bs1 < bs'1

goal :  0bs1 < 0# + 0bs'1
goal = 	subst₂ _<_ (sym eq0) eq1 le
     where
     eq0 :  0bs1 ≡ bs1 * 2bin
     eq0 =  *2≗*2bin bs1

     eq1 = begin bs'1 * 2bin    ≡⟨ sym (*2≗*2bin bs'1) ⟩
                 bs'1 *2        ≡⟨ sym (0+ 0bs'1) ⟩
                 0# + 0bs'1
           ∎

     le :  bs1 * 2bin < bs'1 * 2bin
     le =  *bs1-mono-< [ 0b ] bs1<bs'1
----------------------------------------------

_≤_  is defined as   x ≤ y =  x < y ⊎ x ≡ y.
And imagine that we do not use  suc  for redefining  _≤_.

This is more difficult to compose and to read than the `linear'
construct of
goal =
  begin< 0bs1          (1) ≡[ *2≗*2bin bs1 ]
         bs1 * 2bin    (2) <[ *bs1-mono-< [ 0b ] bs1<bs'1 ]
         bs'1 * 2bin   (3) ≡[ sym (*2≗*2bin bs'1) ]
         bs'1 *2       (4) ≡[ sym (0+ 0bs'1) ]
         0# + 0bs'1    (5)
  end<

Each next term in the column is less or is equal to the current one,
and there is at least one line of the strict construct (that is of
_<[_]_). Hence this proves the goal.

Are there provers in Standard library that enable writing something like
the above `linear' proofs with _<_ ?   

Thanks,

------
Sergei