[Agda] StdLib additions

[Nils Anders Danielsson]

On 2012-11-23 10:36, Peter Divianszky wrote:
> ---------- Data.Nat.Properties
>
> to-from≤ : ∀ {n x} (y : x ≤ n) → toℕ (fromℕ≤ (s≤s y)) ≡ x
> to-from≤ z≤n = refl
> to-from≤ (s≤s y) rewrite to-from≤ y = refl

This definition looks very similar to Data.Fin.Props.toℕ-fromℕ≤.

For information about how to contribute to the library, see the README:

   http://www.cse.chalmers.se/~nad/listings/lib/README.html

(If anyone wonders: I hope to release a new version of the library,
compatible with Agda 2.3.2, soon.)

-- 
/NAD