open Nat doesn't work for Init

Stream: general

[Newell Jensen]

Is there a reason why open Nat doesn't work for what is in Init? I would have thought this would have worked.

import Mathlib

open Nat

-- Doesn't fail
example (m n : Nat) : m < succ n ↔ m ≤ n := Nat.lt_succ_iff

-- Fails witth: unknown identifier 'lt_succ_iff'
example (m n : Nat) : m < succ n ↔ m ≤ n := lt_succ_iff

[Joachim Breitner]

This lemmas is defined using protected:
https://github.com/leanprover/lean4/blob/6fce8f7d5cd18a4419bca7fd51780c71c9b1cc5a/src/Init/Data/Nat/Lemmas.lean#L52-L52
So it always requires the namespace.

Presumably the documentation should include this useful information. @Henrik Böving :-)