[Agda] _iff_ in lib

[Sergei Meshveliani]

People,

I use
  _←→_ : ∀ {α β} (A : Set α) → (B : Set β) → Set (α ⊔ β)  
  _←→_ A B =  (A → B) × (B → A)

as the most general expression for equivalence of two statements.
This allows to save a considerable size in the type signatures of kind  
(p → q , q → p).

But something equivalent is expected to be in Standard library.
For example, how to shortly express in  lib-0.7  the statement

     {m n : ℕ} →  m ≤ n  iff  suc m ≤ suc n
?

Another question is on the syntax. I discover that

1)   _←→_ : ∀ {α β} (A : Set α) (B : Set β) → Set (α ⊔ β)  

     also works, despite that one `→' is forgotten,

2)   _←→_ : ∀ (α β) (A : Set α) → (B : Set β) → Set (α ⊔ β)

     ("forall explicit ...")  is not type-checked.

Is this all right?

Thanks,

------
Sergei