[Agda] +-mono arguments

[Sergei Meshveliani]

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
-------------- next part --------------

  aux : (m n : ℕ) → m + m ≡ 2 + n → m < 2 + n 
  aux 0 _     ()  
  aux (suc m) n  sm+sm≡2+n  with  (2 + m) ≤? (2 + n)
  ... | yes res     = res
  ... | no  ssm≰2+n = ⊥-elim $ sm+sm≢2+n sm+sm≡2+n
                where
                sm = suc m 

                2+n<ssm = ≰→> ssm≰2+n 
                sn≤m    = pred-mono $ pred-mono 2+n<ssm

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

                sm≤sm : sm ≤ sm 
                sm≤sm = ≤refl PE.refl  

                2+n<sm+sm : 3 + n ≤ sm + sm  
                2+n<sm+sm = ≤begin 3 + n     ≤[ 2+n<ssm ] 
                                   1 + sm    ≤[ 1≤sm +-mono sm≤sm ]
                                   sm + sm
                            ≤end

                sm+sm≢2+n : sm + sm ≢ 2 + n
                sm+sm≢2+n = <→≢ 2+n<sm+sm ∘ PE.sym