Nit: I think it's generally preferred to include all the `Require Import`s at the top of the file (or, at least, that is how I've seen it usually done).