Nota concerning scopes : for the first Include, we cannot bind
the scope bigN_scope to a type that doesn't exists yet.
We hence need to explicitely declare the scope substitution.
For the next Include, the abstract type t (in scope abstract_scope)
gets substituted to concrete BigN.t (in scope bigN_scope),
and the corresponding argument scope are fixed automatically.
Notations about
BigN