Cut down on Require Import statements

As discussed at the RT-PROOFS meeting in Braunschweig, the plan is to cut down on the large number of Require Import statements through the judicious use of Require Export, as suggested by Maxime.

CC: @sbozhko