[Agda] +-mono arguments

[Andrés Sicard-Ramírez]

On 22 March 2015 at 12:14, Sergei Meshveliani <mechvel at botik.ru> wrote:
> ----------------------------------------------------------
> 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.

You can replace 1≤sm by `s≤s (z≤n {m})` or `s≤s {n = m} z≤n`.

-- 
Andrés