Don't require nsatz in exp.v

This avoid having coqchk on probability.v report about axioms of the
stdlib (although it still reports about all primitive int and float
primitives, due to coq-elpi offering some interface to them).

theories/exp.v

@@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
 From mathcomp Require Import interval rat.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import mathcomp_extra.
-Require Import reals ereal nsatz_realtype.
+Require Import reals ereal.
 Require Import signed topology normedtype landau sequences derive realfun.
 Require Import itv convex.