[Agda] +-mono arguments

[Sergei Meshveliani]

On Sun, 2015-03-22 at 08:59 -0500, Andrés Sicard-Ramírez wrote:
> Please attach a MCV (minimal, complete and verifiable) example.
> 
> On 22 March 2015 at 07:39, Sergei Meshveliani <mechvel at botik.ru> wrote:
> > Who knows, please,
> > is it possible to cancel below explicit signatures for  1≤sm  and  sm≤sm
> > and to use their values directly as arguments for  _+-mono_
> > ?
> >
> > (see attachment)
> >
> >
> > Thanks,
> >
> > ------
> > Sergei


----------------------------------------------------------
open import Relation.Binary using (module DecTotalOrder)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)

open import Data.Nat using (ℕ; suc; _+_; _≤_; _<_; s≤s; z≤n;
                                   decTotalOrder; module ≤-Reasoning)
open import Data.Nat.Properties using (_+-mono_)
open ≤-Reasoning using () renaming (begin_ to ≤begin_; _∎ to _≤end;
                                _≡⟨_⟩_ to _≡≤[_]_; _≤⟨_⟩_ to _≤[_]_)

≤refl = DecTotalOrder.reflexive decTotalOrder

foo : (m n : ℕ) → 2 + n < 2 + m → 3 + n ≤ suc m + suc m
foo m n 2+n<2+m =
            ≤begin 3 + n       ≤[ 2+n<2+m ]
                   2 + m      ≡≤[ PE.refl ]
                   1 + sm      ≤[ 1≤sm +-mono (≤refl PE.refl) ]
                   sm + sm        
            ≤end
            where  sm = suc m

                   1≤sm : 1 ≤ sm
                   1≤sm = s≤s z≤n
---------------------------------------------------------

After simplification the second argument in  +-mono  has improved
(I do not know, why).
And  1≤sm  remains,  it needs explicit signature.

Thanks,

------
Sergei