Is it possible to import a file in a proof only in Coq?

I'm looking for something like this

Suppose I have a lemma that is using some long named module

Lemma foo : SomeLongNamedModule.foo = blablabla.

I want to import SomeLongNamedModule inside the proof but left scope outside of the proof clean. I'm looking for something like this

Lemma foo : SomeLongNamedModule.foo = blablabla
  Local Import SomeLongNamedModule
  ...

Qed

(* Here SomeLongNamedModule is not polluting the scope *)

Is that possible? I think about wrapping it in a module but it seems overkill to me. To explain my use case, I'm working on a code base where we avoid Import, but during the writing of proofs I insert the Import and then remove it later and refactor the proof. If there is something Local Import it would be possible left it there in some cases.

One option is using modules, this works

Module Bar.
  Parameter bar : forall {A : Type}, A -> A.
End Bar.

Module Foo.
  Import Bar.

  Check bar.
End Foo.

Fail Check bar. (* bar not defined here *)

My guess is that Lemma is not a scope so I can't do this.