diff options
Diffstat (limited to 'theories/Reals/TAF.v')
| -rw-r--r-- | theories/Reals/TAF.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/TAF.v b/theories/Reals/TAF.v index 2bcbf55d9..d797bb7d5 100644 --- a/theories/Reals/TAF.v +++ b/theories/Reals/TAF.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Ranalysis1. Require Rtopology. @@ -515,4 +515,4 @@ Assert H9 : ``a<=x0<=b``. Split; Left; Assumption. Apply derivable_pt_lim_minus; [Elim (H ? H9) | Elim (H0 ? H9)]; Intros; EApply derive_pt_eq_1; Symmetry; Apply H10. Assert H8 := (null_derivative_loc (minus_fct g1 g2) a b H5 H6 H7); Unfold constant_D_eq in H8; Assert H9 := (H8 ? H2); Unfold minus_fct in H9; Rewrite <- H9; Ring. -Qed.
\ No newline at end of file +Qed. |