fix

Author: mkerjean

theories/hahn_banach_theorem.v

@@ -335,6 +335,7 @@ End HBPreparation.
 
 Section HahnBanach.
 Import Lingraph.
+Import HBPreparation.  
 (* Now we prove HahnBanach on functions*)
 (* We consider R a real (=ordered) field with supremum, and V a (left) module
    on R. We do not make use of the 'vector' interface as the latter enforces