I presume though that Mathlib does not define the extended naturals? If they did then 1:N / 0:N would be valued at this infinity.

What I found interesting about the Scott encoding was that natural infinity was trivial to define, and arises directly from a straightforward construction of the div function (for naturals).

The encoding is as follows (\x indicates lambda abstraction for identifier x. Recursion is assumed, of course it could be made explicit with the Y combinator):

  zero := \f \x n
  succ := \n \f \x f n

  infinite := \n succ (infinite n)
  infinity := infinite zero

  subn := \n \m m (\p n (\q subn q p) n) n

  divn := \n \m (subn m n) (\p zero) (succ (divn (subn n m) m))

  divn (succ zero) zero => infinity

EDIT: Note that infinity does not have a normal form (does not terminate), but:

  subn n infinity => zero