Fixed proof of irrelevance of le on nat, inspired by the
corresponding proof in ssreflect.